interpretationObjs3579(pinup,[objects(person,[p1,p2,p3,p4,p5,p6]),objects(floor,[top,f1,bottom]),objects(maxobj,[a,a1])]).

interpretations3579(pinup,[[[at,at(top)],[not_at,not_at(f1),not_at(bottom)],[pup,pup(p2,f1)],[not_pup,not_pup(p1,top),not_pup(p1,f1),not_pup(p1,bottom),not_pup(p2,top),not_pup(p2,bottom),not_pup(p3,top),not_pup(p3,f1),not_pup(p3,bottom),not_pup(p4,top),not_pup(p4,f1),not_pup(p4,bottom),not_pup(p5,top),not_pup(p5,f1),not_pup(p5,bottom),not_pup(p6,top),not_pup(p6,f1),not_pup(p6,bottom)],[pdown],[not_pdown,not_pdown(p1,top),not_pdown(p1,f1),not_pdown(p1,bottom),not_pdown(p2,top),not_pdown(p2,f1),not_pdown(p2,bottom),not_pdown(p3,top),not_pdown(p3,f1),not_pdown(p3,bottom),not_pdown(p4,top),not_pdown(p4,f1),not_pdown(p4,bottom),not_pdown(p5,top),not_pdown(p5,f1),not_pdown(p5,bottom),not_pdown(p6,top),not_pdown(p6,f1),not_pdown(p6,bottom)],[above,above(top,bottom),above(top,f1),above(f1,bottom)],[not_above,not_above(top,top),not_above(f1,top),not_above(f1,f1),not_above(bottom,top),not_above(bottom,f1),not_above(bottom,bottom)],[pinup,pinup(p5)],[not_pinup,not_pinup(p1),not_pinup(p2),not_pinup(p3),not_pinup(p4),not_pinup(p6)],[pindown,pindown(p6)],[not_pindown,not_pindown(p1),not_pindown(p2),not_pindown(p3),not_pindown(p4),not_pindown(p5)],[up],[not_up,not_up],[eq,eq(p1,p1),eq(p2,p2),eq(p3,p3),eq(p4,p4),eq(p5,p5),eq(p6,p6),eq(top,top),eq(f1,f1),eq(bottom,bottom),eq(a,a),eq(a1,a1)],[not_eq,not_eq(p1,p2),not_eq(p1,p3),not_eq(p1,p4),not_eq(p1,p5),not_eq(p1,p6),not_eq(p2,p1),not_eq(p2,p3),not_eq(p2,p4),not_eq(p2,p5),not_eq(p2,p6),not_eq(p3,p1),not_eq(p3,p2),not_eq(p3,p4),not_eq(p3,p5),not_eq(p3,p6),not_eq(p4,p1),not_eq(p4,p2),not_eq(p4,p3),not_eq(p4,p5),not_eq(p4,p6),not_eq(p5,p1),not_eq(p5,p2),not_eq(p5,p3),not_eq(p5,p4),not_eq(p5,p6),not_eq(p6,p1),not_eq(p6,p2),not_eq(p6,p3),not_eq(p6,p4),not_eq(p6,p5),not_eq(top,f1),not_eq(top,bottom),not_eq(f1,top),not_eq(f1,bottom),not_eq(bottom,top),not_eq(bottom,f1),not_eq(a,a1),not_eq(a1,a)]],[[at,at(f1)],[not_at,not_at(top),not_at(bottom)],[pup,pup(p2,f1)],[not_pup,not_pup(p1,top),not_pup(p1,f1),not_pup(p1,bottom),not_pup(p2,top),not_pup(p2,bottom),not_pup(p3,top),not_pup(p3,f1),not_pup(p3,bottom),not_pup(p4,top),not_pup(p4,f1),not_pup(p4,bottom),not_pup(p5,top),not_pup(p5,f1),not_pup(p5,bottom),not_pup(p6,top),not_pup(p6,f1),not_pup(p6,bottom)],[pdown,pdown(p3,f1)],[not_pdown,not_pdown(p1,top),not_pdown(p1,f1),not_pdown(p1,bottom),not_pdown(p2,top),not_pdown(p2,f1),not_pdown(p2,bottom),not_pdown(p3,top),not_pdown(p3,bottom),not_pdown(p4,top),not_pdown(p4,f1),not_pdown(p4,bottom),not_pdown(p5,top),not_pdown(p5,f1),not_pdown(p5,bottom),not_pdown(p6,top),not_pdown(p6,f1),not_pdown(p6,bottom)],[above,above(top,bottom),above(top,f1),above(f1,bottom)],[not_above,not_above(top,top),not_above(f1,top),not_above(f1,f1),not_above(bottom,top),not_above(bottom,f1),not_above(bottom,bottom)],[pinup,pinup(p5)],[not_pinup,not_pinup(p1),not_pinup(p2),not_pinup(p3),not_pinup(p4),not_pinup(p6)],[pindown,pindown(p6)],[not_pindown,not_pindown(p1),not_pindown(p2),not_pindown(p3),not_pindown(p4),not_pindown(p5)],[up],[not_up,not_up],[eq,eq(p1,p1),eq(p2,p2),eq(p3,p3),eq(p4,p4),eq(p5,p5),eq(p6,p6),eq(top,top),eq(f1,f1),eq(bottom,bottom),eq(a,a),eq(a1,a1)],[not_eq,not_eq(p1,p2),not_eq(p1,p3),not_eq(p1,p4),not_eq(p1,p5),not_eq(p1,p6),not_eq(p2,p1),not_eq(p2,p3),not_eq(p2,p4),not_eq(p2,p5),not_eq(p2,p6),not_eq(p3,p1),not_eq(p3,p2),not_eq(p3,p4),not_eq(p3,p5),not_eq(p3,p6),not_eq(p4,p1),not_eq(p4,p2),not_eq(p4,p3),not_eq(p4,p5),not_eq(p4,p6),not_eq(p5,p1),not_eq(p5,p2),not_eq(p5,p3),not_eq(p5,p4),not_eq(p5,p6),not_eq(p6,p1),not_eq(p6,p2),not_eq(p6,p3),not_eq(p6,p4),not_eq(p6,p5),not_eq(top,f1),not_eq(top,bottom),not_eq(f1,top),not_eq(f1,bottom),not_eq(bottom,top),not_eq(bottom,f1),not_eq(a,a1),not_eq(a1,a)]],[[at,at(f1)],[not_at,not_at(top),not_at(bottom)],[pup,pup(p1,bottom),pup(p2,f1)],[not_pup,not_pup(p1,top),not_pup(p1,f1),not_pup(p2,top),not_pup(p2,bottom),not_pup(p3,top),not_pup(p3,f1),not_pup(p3,bottom),not_pup(p4,top),not_pup(p4,f1),not_pup(p4,bottom),not_pup(p5,top),not_pup(p5,f1),not_pup(p5,bottom),not_pup(p6,top),not_pup(p6,f1),not_pup(p6,bottom)],[pdown],[not_pdown,not_pdown(p1,top),not_pdown(p1,f1),not_pdown(p1,bottom),not_pdown(p2,top),not_pdown(p2,f1),not_pdown(p2,bottom),not_pdown(p3,top),not_pdown(p3,f1),not_pdown(p3,bottom),not_pdown(p4,top),not_pdown(p4,f1),not_pdown(p4,bottom),not_pdown(p5,top),not_pdown(p5,f1),not_pdown(p5,bottom),not_pdown(p6,top),not_pdown(p6,f1),not_pdown(p6,bottom)],[above,above(top,bottom),above(top,f1),above(f1,bottom)],[not_above,not_above(top,top),not_above(f1,top),not_above(f1,f1),not_above(bottom,top),not_above(bottom,f1),not_above(bottom,bottom)],[pinup],[not_pinup,not_pinup(p1),not_pinup(p2),not_pinup(p3),not_pinup(p4),not_pinup(p5),not_pinup(p6)],[pindown,pindown(p6)],[not_pindown,not_pindown(p1),not_pindown(p2),not_pindown(p3),not_pindown(p4),not_pindown(p5)],[up],[not_up,not_up],[eq,eq(p1,p1),eq(p2,p2),eq(p3,p3),eq(p4,p4),eq(p5,p5),eq(p6,p6),eq(top,top),eq(f1,f1),eq(bottom,bottom),eq(a,a),eq(a1,a1)],[not_eq,not_eq(p1,p2),not_eq(p1,p3),not_eq(p1,p4),not_eq(p1,p5),not_eq(p1,p6),not_eq(p2,p1),not_eq(p2,p3),not_eq(p2,p4),not_eq(p2,p5),not_eq(p2,p6),not_eq(p3,p1),not_eq(p3,p2),not_eq(p3,p4),not_eq(p3,p5),not_eq(p3,p6),not_eq(p4,p1),not_eq(p4,p2),not_eq(p4,p3),not_eq(p4,p5),not_eq(p4,p6),not_eq(p5,p1),not_eq(p5,p2),not_eq(p5,p3),not_eq(p5,p4),not_eq(p5,p6),not_eq(p6,p1),not_eq(p6,p2),not_eq(p6,p3),not_eq(p6,p4),not_eq(p6,p5),not_eq(top,f1),not_eq(top,bottom),not_eq(f1,top),not_eq(f1,bottom),not_eq(bottom,top),not_eq(bottom,f1),not_eq(a,a1),not_eq(a1,a)]],[[at,at(bottom)],[not_at,not_at(top),not_at(f1)],[pup,pup(p1,bottom)],[not_pup,not_pup(p1,top),not_pup(p1,f1),not_pup(p2,top),not_pup(p2,f1),not_pup(p2,bottom),not_pup(p3,top),not_pup(p3,f1),not_pup(p3,bottom),not_pup(p4,top),not_pup(p4,f1),not_pup(p4,bottom),not_pup(p5,top),not_pup(p5,f1),not_pup(p5,bottom),not_pup(p6,top),not_pup(p6,f1),not_pup(p6,bottom)],[pdown,pdown(p3,f1),pdown(p4,top)],[not_pdown,not_pdown(p1,top),not_pdown(p1,f1),not_pdown(p1,bottom),not_pdown(p2,top),not_pdown(p2,f1),not_pdown(p2,bottom),not_pdown(p3,top),not_pdown(p3,bottom),not_pdown(p4,f1),not_pdown(p4,bottom),not_pdown(p5,top),not_pdown(p5,f1),not_pdown(p5,bottom),not_pdown(p6,top),not_pdown(p6,f1),not_pdown(p6,bottom)],[above,above(top,bottom),above(top,f1),above(f1,bottom)],[not_above,not_above(top,top),not_above(f1,top),not_above(f1,f1),not_above(bottom,top),not_above(bottom,f1),not_above(bottom,bottom)],[pinup,pinup(p5)],[not_pinup,not_pinup(p1),not_pinup(p2),not_pinup(p3),not_pinup(p4),not_pinup(p6)],[pindown],[not_pindown,not_pindown(p1),not_pindown(p2),not_pindown(p3),not_pindown(p4),not_pindown(p5),not_pindown(p6)],[up],[not_up,not_up],[eq,eq(p1,p1),eq(p2,p2),eq(p3,p3),eq(p4,p4),eq(p5,p5),eq(p6,p6),eq(top,top),eq(f1,f1),eq(bottom,bottom),eq(a,a),eq(a1,a1)],[not_eq,not_eq(p1,p2),not_eq(p1,p3),not_eq(p1,p4),not_eq(p1,p5),not_eq(p1,p6),not_eq(p2,p1),not_eq(p2,p3),not_eq(p2,p4),not_eq(p2,p5),not_eq(p2,p6),not_eq(p3,p1),not_eq(p3,p2),not_eq(p3,p4),not_eq(p3,p5),not_eq(p3,p6),not_eq(p4,p1),not_eq(p4,p2),not_eq(p4,p3),not_eq(p4,p5),not_eq(p4,p6),not_eq(p5,p1),not_eq(p5,p2),not_eq(p5,p3),not_eq(p5,p4),not_eq(p5,p6),not_eq(p6,p1),not_eq(p6,p2),not_eq(p6,p3),not_eq(p6,p4),not_eq(p6,p5),not_eq(top,f1),not_eq(top,bottom),not_eq(f1,top),not_eq(f1,bottom),not_eq(bottom,top),not_eq(bottom,f1),not_eq(a,a1),not_eq(a1,a)]],[[at,at(bottom)],[not_at,not_at(top),not_at(f1)],[pup,pup(p1,bottom)],[not_pup,not_pup(p1,top),not_pup(p1,f1),not_pup(p2,top),not_pup(p2,f1),not_pup(p2,bottom),not_pup(p3,top),not_pup(p3,f1),not_pup(p3,bottom),not_pup(p4,top),not_pup(p4,f1),not_pup(p4,bottom),not_pup(p5,top),not_pup(p5,f1),not_pup(p5,bottom),not_pup(p6,top),not_pup(p6,f1),not_pup(p6,bottom)],[pdown],[not_pdown,not_pdown(p1,top),not_pdown(p1,f1),not_pdown(p1,bottom),not_pdown(p2,top),not_pdown(p2,f1),not_pdown(p2,bottom),not_pdown(p3,top),not_pdown(p3,f1),not_pdown(p3,bottom),not_pdown(p4,top),not_pdown(p4,f1),not_pdown(p4,bottom),not_pdown(p5,top),not_pdown(p5,f1),not_pdown(p5,bottom),not_pdown(p6,top),not_pdown(p6,f1),not_pdown(p6,bottom)],[above,above(top,bottom),above(top,f1),above(f1,bottom)],[not_above,not_above(top,top),not_above(f1,top),not_above(f1,f1),not_above(bottom,top),not_above(bottom,f1),not_above(bottom,bottom)],[pinup],[not_pinup,not_pinup(p1),not_pinup(p2),not_pinup(p3),not_pinup(p4),not_pinup(p5),not_pinup(p6)],[pindown,pindown(p6)],[not_pindown,not_pindown(p1),not_pindown(p2),not_pindown(p3),not_pindown(p4),not_pindown(p5)],[up],[not_up,not_up],[eq,eq(p1,p1),eq(p2,p2),eq(p3,p3),eq(p4,p4),eq(p5,p5),eq(p6,p6),eq(top,top),eq(f1,f1),eq(bottom,bottom),eq(a,a),eq(a1,a1)],[not_eq,not_eq(p1,p2),not_eq(p1,p3),not_eq(p1,p4),not_eq(p1,p5),not_eq(p1,p6),not_eq(p2,p1),not_eq(p2,p3),not_eq(p2,p4),not_eq(p2,p5),not_eq(p2,p6),not_eq(p3,p1),not_eq(p3,p2),not_eq(p3,p4),not_eq(p3,p5),not_eq(p3,p6),not_eq(p4,p1),not_eq(p4,p2),not_eq(p4,p3),not_eq(p4,p5),not_eq(p4,p6),not_eq(p5,p1),not_eq(p5,p2),not_eq(p5,p3),not_eq(p5,p4),not_eq(p5,p6),not_eq(p6,p1),not_eq(p6,p2),not_eq(p6,p3),not_eq(p6,p4),not_eq(p6,p5),not_eq(top,f1),not_eq(top,bottom),not_eq(f1,top),not_eq(f1,bottom),not_eq(bottom,top),not_eq(bottom,f1),not_eq(a,a1),not_eq(a1,a)]],[[at,at(top)],[not_at,not_at(f1),not_at(bottom)],[pup,pup(p1,bottom)],[not_pup,not_pup(p1,top),not_pup(p1,f1),not_pup(p2,top),not_pup(p2,f1),not_pup(p2,bottom),not_pup(p3,top),not_pup(p3,f1),not_pup(p3,bottom),not_pup(p4,top),not_pup(p4,f1),not_pup(p4,bottom),not_pup(p5,top),not_pup(p5,f1),not_pup(p5,bottom),not_pup(p6,top),not_pup(p6,f1),not_pup(p6,bottom)],[pdown,pdown(p3,f1)],[not_pdown,not_pdown(p1,top),not_pdown(p1,f1),not_pdown(p1,bottom),not_pdown(p2,top),not_pdown(p2,f1),not_pdown(p2,bottom),not_pdown(p3,top),not_pdown(p3,bottom),not_pdown(p4,top),not_pdown(p4,f1),not_pdown(p4,bottom),not_pdown(p5,top),not_pdown(p5,f1),not_pdown(p5,bottom),not_pdown(p6,top),not_pdown(p6,f1),not_pdown(p6,bottom)],[above,above(top,bottom),above(top,f1),above(f1,bottom)],[not_above,not_above(top,top),not_above(f1,top),not_above(f1,f1),not_above(bottom,top),not_above(bottom,f1),not_above(bottom,bottom)],[pinup],[not_pinup,not_pinup(p1),not_pinup(p2),not_pinup(p3),not_pinup(p4),not_pinup(p5),not_pinup(p6)],[pindown,pindown(p6)],[not_pindown,not_pindown(p1),not_pindown(p2),not_pindown(p3),not_pindown(p4),not_pindown(p5)],[up],[not_up,not_up],[eq,eq(p1,p1),eq(p2,p2),eq(p3,p3),eq(p4,p4),eq(p5,p5),eq(p6,p6),eq(top,top),eq(f1,f1),eq(bottom,bottom),eq(a,a),eq(a1,a1)],[not_eq,not_eq(p1,p2),not_eq(p1,p3),not_eq(p1,p4),not_eq(p1,p5),not_eq(p1,p6),not_eq(p2,p1),not_eq(p2,p3),not_eq(p2,p4),not_eq(p2,p5),not_eq(p2,p6),not_eq(p3,p1),not_eq(p3,p2),not_eq(p3,p4),not_eq(p3,p5),not_eq(p3,p6),not_eq(p4,p1),not_eq(p4,p2),not_eq(p4,p3),not_eq(p4,p5),not_eq(p4,p6),not_eq(p5,p1),not_eq(p5,p2),not_eq(p5,p3),not_eq(p5,p4),not_eq(p5,p6),not_eq(p6,p1),not_eq(p6,p2),not_eq(p6,p3),not_eq(p6,p4),not_eq(p6,p5),not_eq(top,f1),not_eq(top,bottom),not_eq(f1,top),not_eq(f1,bottom),not_eq(bottom,top),not_eq(bottom,f1),not_eq(a,a1),not_eq(a1,a)]],[[at,at(bottom)],[not_at,not_at(top),not_at(f1)],[pup],[not_pup,not_pup(p1,top),not_pup(p1,f1),not_pup(p1,bottom),not_pup(p2,top),not_pup(p2,f1),not_pup(p2,bottom),not_pup(p3,top),not_pup(p3,f1),not_pup(p3,bottom),not_pup(p4,top),not_pup(p4,f1),not_pup(p4,bottom),not_pup(p5,top),not_pup(p5,f1),not_pup(p5,bottom),not_pup(p6,top),not_pup(p6,f1),not_pup(p6,bottom)],[pdown,pdown(p3,f1)],[not_pdown,not_pdown(p1,top),not_pdown(p1,f1),not_pdown(p1,bottom),not_pdown(p2,top),not_pdown(p2,f1),not_pdown(p2,bottom),not_pdown(p3,top),not_pdown(p3,bottom),not_pdown(p4,top),not_pdown(p4,f1),not_pdown(p4,bottom),not_pdown(p5,top),not_pdown(p5,f1),not_pdown(p5,bottom),not_pdown(p6,top),not_pdown(p6,f1),not_pdown(p6,bottom)],[above,above(top,bottom),above(top,f1),above(f1,bottom)],[not_above,not_above(top,top),not_above(f1,top),not_above(f1,f1),not_above(bottom,top),not_above(bottom,f1),not_above(bottom,bottom)],[pinup,pinup(p5)],[not_pinup,not_pinup(p1),not_pinup(p2),not_pinup(p3),not_pinup(p4),not_pinup(p6)],[pindown,pindown(p6)],[not_pindown,not_pindown(p1),not_pindown(p2),not_pindown(p3),not_pindown(p4),not_pindown(p5)],[up],[not_up,not_up],[eq,eq(p1,p1),eq(p2,p2),eq(p3,p3),eq(p4,p4),eq(p5,p5),eq(p6,p6),eq(top,top),eq(f1,f1),eq(bottom,bottom),eq(a,a),eq(a1,a1)],[not_eq,not_eq(p1,p2),not_eq(p1,p3),not_eq(p1,p4),not_eq(p1,p5),not_eq(p1,p6),not_eq(p2,p1),not_eq(p2,p3),not_eq(p2,p4),not_eq(p2,p5),not_eq(p2,p6),not_eq(p3,p1),not_eq(p3,p2),not_eq(p3,p4),not_eq(p3,p5),not_eq(p3,p6),not_eq(p4,p1),not_eq(p4,p2),not_eq(p4,p3),not_eq(p4,p5),not_eq(p4,p6),not_eq(p5,p1),not_eq(p5,p2),not_eq(p5,p3),not_eq(p5,p4),not_eq(p5,p6),not_eq(p6,p1),not_eq(p6,p2),not_eq(p6,p3),not_eq(p6,p4),not_eq(p6,p5),not_eq(top,f1),not_eq(top,bottom),not_eq(f1,top),not_eq(f1,bottom),not_eq(bottom,top),not_eq(bottom,f1),not_eq(a,a1),not_eq(a1,a)]],[[at,at(f1)],[not_at,not_at(top),not_at(bottom)],[pup,pup(p2,f1)],[not_pup,not_pup(p1,top),not_pup(p1,f1),not_pup(p1,bottom),not_pup(p2,top),not_pup(p2,bottom),not_pup(p3,top),not_pup(p3,f1),not_pup(p3,bottom),not_pup(p4,top),not_pup(p4,f1),not_pup(p4,bottom),not_pup(p5,top),not_pup(p5,f1),not_pup(p5,bottom),not_pup(p6,top),not_pup(p6,f1),not_pup(p6,bottom)],[pdown,pdown(p4,top)],[not_pdown,not_pdown(p1,top),not_pdown(p1,f1),not_pdown(p1,bottom),not_pdown(p2,top),not_pdown(p2,f1),not_pdown(p2,bottom),not_pdown(p3,top),not_pdown(p3,f1),not_pdown(p3,bottom),not_pdown(p4,f1),not_pdown(p4,bottom),not_pdown(p5,top),not_pdown(p5,f1),not_pdown(p5,bottom),not_pdown(p6,top),not_pdown(p6,f1),not_pdown(p6,bottom)],[above,above(top,bottom),above(top,f1),above(f1,bottom)],[not_above,not_above(top,top),not_above(f1,top),not_above(f1,f1),not_above(bottom,top),not_above(bottom,f1),not_above(bottom,bottom)],[pinup,pinup(p5)],[not_pinup,not_pinup(p1),not_pinup(p2),not_pinup(p3),not_pinup(p4),not_pinup(p6)],[pindown],[not_pindown,not_pindown(p1),not_pindown(p2),not_pindown(p3),not_pindown(p4),not_pindown(p5),not_pindown(p6)],[up],[not_up,not_up],[eq,eq(p1,p1),eq(p2,p2),eq(p3,p3),eq(p4,p4),eq(p5,p5),eq(p6,p6),eq(top,top),eq(f1,f1),eq(bottom,bottom),eq(a,a),eq(a1,a1)],[not_eq,not_eq(p1,p2),not_eq(p1,p3),not_eq(p1,p4),not_eq(p1,p5),not_eq(p1,p6),not_eq(p2,p1),not_eq(p2,p3),not_eq(p2,p4),not_eq(p2,p5),not_eq(p2,p6),not_eq(p3,p1),not_eq(p3,p2),not_eq(p3,p4),not_eq(p3,p5),not_eq(p3,p6),not_eq(p4,p1),not_eq(p4,p2),not_eq(p4,p3),not_eq(p4,p5),not_eq(p4,p6),not_eq(p5,p1),not_eq(p5,p2),not_eq(p5,p3),not_eq(p5,p4),not_eq(p5,p6),not_eq(p6,p1),not_eq(p6,p2),not_eq(p6,p3),not_eq(p6,p4),not_eq(p6,p5),not_eq(top,f1),not_eq(top,bottom),not_eq(f1,top),not_eq(f1,bottom),not_eq(bottom,top),not_eq(bottom,f1),not_eq(a,a1),not_eq(a1,a)]],[[at,at(bottom)],[not_at,not_at(top),not_at(f1)],[pup,pup(p2,f1)],[not_pup,not_pup(p1,top),not_pup(p1,f1),not_pup(p1,bottom),not_pup(p2,top),not_pup(p2,bottom),not_pup(p3,top),not_pup(p3,f1),not_pup(p3,bottom),not_pup(p4,top),not_pup(p4,f1),not_pup(p4,bottom),not_pup(p5,top),not_pup(p5,f1),not_pup(p5,bottom),not_pup(p6,top),not_pup(p6,f1),not_pup(p6,bottom)],[pdown],[not_pdown,not_pdown(p1,top),not_pdown(p1,f1),not_pdown(p1,bottom),not_pdown(p2,top),not_pdown(p2,f1),not_pdown(p2,bottom),not_pdown(p3,top),not_pdown(p3,f1),not_pdown(p3,bottom),not_pdown(p4,top),not_pdown(p4,f1),not_pdown(p4,bottom),not_pdown(p5,top),not_pdown(p5,f1),not_pdown(p5,bottom),not_pdown(p6,top),not_pdown(p6,f1),not_pdown(p6,bottom)],[above,above(top,bottom),above(top,f1),above(f1,bottom)],[not_above,not_above(top,top),not_above(f1,top),not_above(f1,f1),not_above(bottom,top),not_above(bottom,f1),not_above(bottom,bottom)],[pinup,pinup(p5)],[not_pinup,not_pinup(p1),not_pinup(p2),not_pinup(p3),not_pinup(p4),not_pinup(p6)],[pindown],[not_pindown,not_pindown(p1),not_pindown(p2),not_pindown(p3),not_pindown(p4),not_pindown(p5),not_pindown(p6)],[up],[not_up,not_up],[eq,eq(p1,p1),eq(p2,p2),eq(p3,p3),eq(p4,p4),eq(p5,p5),eq(p6,p6),eq(top,top),eq(f1,f1),eq(bottom,bottom),eq(a,a),eq(a1,a1)],[not_eq,not_eq(p1,p2),not_eq(p1,p3),not_eq(p1,p4),not_eq(p1,p5),not_eq(p1,p6),not_eq(p2,p1),not_eq(p2,p3),not_eq(p2,p4),not_eq(p2,p5),not_eq(p2,p6),not_eq(p3,p1),not_eq(p3,p2),not_eq(p3,p4),not_eq(p3,p5),not_eq(p3,p6),not_eq(p4,p1),not_eq(p4,p2),not_eq(p4,p3),not_eq(p4,p5),not_eq(p4,p6),not_eq(p5,p1),not_eq(p5,p2),not_eq(p5,p3),not_eq(p5,p4),not_eq(p5,p6),not_eq(p6,p1),not_eq(p6,p2),not_eq(p6,p3),not_eq(p6,p4),not_eq(p6,p5),not_eq(top,f1),not_eq(top,bottom),not_eq(f1,top),not_eq(f1,bottom),not_eq(bottom,top),not_eq(bottom,f1),not_eq(a,a1),not_eq(a1,a)]],[[at,at(top)],[not_at,not_at(f1),not_at(bottom)],[pup],[not_pup,not_pup(p1,top),not_pup(p1,f1),not_pup(p1,bottom),not_pup(p2,top),not_pup(p2,f1),not_pup(p2,bottom),not_pup(p3,top),not_pup(p3,f1),not_pup(p3,bottom),not_pup(p4,top),not_pup(p4,f1),not_pup(p4,bottom),not_pup(p5,top),not_pup(p5,f1),not_pup(p5,bottom),not_pup(p6,top),not_pup(p6,f1),not_pup(p6,bottom)],[pdown,pdown(p4,top)],[not_pdown,not_pdown(p1,top),not_pdown(p1,f1),not_pdown(p1,bottom),not_pdown(p2,top),not_pdown(p2,f1),not_pdown(p2,bottom),not_pdown(p3,top),not_pdown(p3,f1),not_pdown(p3,bottom),not_pdown(p4,f1),not_pdown(p4,bottom),not_pdown(p5,top),not_pdown(p5,f1),not_pdown(p5,bottom),not_pdown(p6,top),not_pdown(p6,f1),not_pdown(p6,bottom)],[above,above(top,bottom),above(top,f1),above(f1,bottom)],[not_above,not_above(top,top),not_above(f1,top),not_above(f1,f1),not_above(bottom,top),not_above(bottom,f1),not_above(bottom,bottom)],[pinup,pinup(p5)],[not_pinup,not_pinup(p1),not_pinup(p2),not_pinup(p3),not_pinup(p4),not_pinup(p6)],[pindown,pindown(p6)],[not_pindown,not_pindown(p1),not_pindown(p2),not_pindown(p3),not_pindown(p4),not_pindown(p5)],[up],[not_up,not_up],[eq,eq(p1,p1),eq(p2,p2),eq(p3,p3),eq(p4,p4),eq(p5,p5),eq(p6,p6),eq(top,top),eq(f1,f1),eq(bottom,bottom),eq(a,a),eq(a1,a1)],[not_eq,not_eq(p1,p2),not_eq(p1,p3),not_eq(p1,p4),not_eq(p1,p5),not_eq(p1,p6),not_eq(p2,p1),not_eq(p2,p3),not_eq(p2,p4),not_eq(p2,p5),not_eq(p2,p6),not_eq(p3,p1),not_eq(p3,p2),not_eq(p3,p4),not_eq(p3,p5),not_eq(p3,p6),not_eq(p4,p1),not_eq(p4,p2),not_eq(p4,p3),not_eq(p4,p5),not_eq(p4,p6),not_eq(p5,p1),not_eq(p5,p2),not_eq(p5,p3),not_eq(p5,p4),not_eq(p5,p6),not_eq(p6,p1),not_eq(p6,p2),not_eq(p6,p3),not_eq(p6,p4),not_eq(p6,p5),not_eq(top,f1),not_eq(top,bottom),not_eq(f1,top),not_eq(f1,bottom),not_eq(bottom,top),not_eq(bottom,f1),not_eq(a,a1),not_eq(a1,a)]],[[at,at(top)],[not_at,not_at(f1),not_at(bottom)],[pup,pup(p2,f1)],[not_pup,not_pup(p1,top),not_pup(p1,f1),not_pup(p1,bottom),not_pup(p2,top),not_pup(p2,bottom),not_pup(p3,top),not_pup(p3,f1),not_pup(p3,bottom),not_pup(p4,top),not_pup(p4,f1),not_pup(p4,bottom),not_pup(p5,top),not_pup(p5,f1),not_pup(p5,bottom),not_pup(p6,top),not_pup(p6,f1),not_pup(p6,bottom)],[pdown,pdown(p3,f1),pdown(p4,top)],[not_pdown,not_pdown(p1,top),not_pdown(p1,f1),not_pdown(p1,bottom),not_pdown(p2,top),not_pdown(p2,f1),not_pdown(p2,bottom),not_pdown(p3,top),not_pdown(p3,bottom),not_pdown(p4,f1),not_pdown(p4,bottom),not_pdown(p5,top),not_pdown(p5,f1),not_pdown(p5,bottom),not_pdown(p6,top),not_pdown(p6,f1),not_pdown(p6,bottom)],[above,above(top,bottom),above(top,f1),above(f1,bottom)],[not_above,not_above(top,top),not_above(f1,top),not_above(f1,f1),not_above(bottom,top),not_above(bottom,f1),not_above(bottom,bottom)],[pinup],[not_pinup,not_pinup(p1),not_pinup(p2),not_pinup(p3),not_pinup(p4),not_pinup(p5),not_pinup(p6)],[pindown],[not_pindown,not_pindown(p1),not_pindown(p2),not_pindown(p3),not_pindown(p4),not_pindown(p5),not_pindown(p6)],[up],[not_up,not_up],[eq,eq(p1,p1),eq(p2,p2),eq(p3,p3),eq(p4,p4),eq(p5,p5),eq(p6,p6),eq(top,top),eq(f1,f1),eq(bottom,bottom),eq(a,a),eq(a1,a1)],[not_eq,not_eq(p1,p2),not_eq(p1,p3),not_eq(p1,p4),not_eq(p1,p5),not_eq(p1,p6),not_eq(p2,p1),not_eq(p2,p3),not_eq(p2,p4),not_eq(p2,p5),not_eq(p2,p6),not_eq(p3,p1),not_eq(p3,p2),not_eq(p3,p4),not_eq(p3,p5),not_eq(p3,p6),not_eq(p4,p1),not_eq(p4,p2),not_eq(p4,p3),not_eq(p4,p5),not_eq(p4,p6),not_eq(p5,p1),not_eq(p5,p2),not_eq(p5,p3),not_eq(p5,p4),not_eq(p5,p6),not_eq(p6,p1),not_eq(p6,p2),not_eq(p6,p3),not_eq(p6,p4),not_eq(p6,p5),not_eq(top,f1),not_eq(top,bottom),not_eq(f1,top),not_eq(f1,bottom),not_eq(bottom,top),not_eq(bottom,f1),not_eq(a,a1),not_eq(a1,a)]],[[at,at(f1)],[not_at,not_at(top),not_at(bottom)],[pup,pup(p1,bottom)],[not_pup,not_pup(p1,top),not_pup(p1,f1),not_pup(p2,top),not_pup(p2,f1),not_pup(p2,bottom),not_pup(p3,top),not_pup(p3,f1),not_pup(p3,bottom),not_pup(p4,top),not_pup(p4,f1),not_pup(p4,bottom),not_pup(p5,top),not_pup(p5,f1),not_pup(p5,bottom),not_pup(p6,top),not_pup(p6,f1),not_pup(p6,bottom)],[pdown],[not_pdown,not_pdown(p1,top),not_pdown(p1,f1),not_pdown(p1,bottom),not_pdown(p2,top),not_pdown(p2,f1),not_pdown(p2,bottom),not_pdown(p3,top),not_pdown(p3,f1),not_pdown(p3,bottom),not_pdown(p4,top),not_pdown(p4,f1),not_pdown(p4,bottom),not_pdown(p5,top),not_pdown(p5,f1),not_pdown(p5,bottom),not_pdown(p6,top),not_pdown(p6,f1),not_pdown(p6,bottom)],[above,above(top,bottom),above(top,f1),above(f1,bottom)],[not_above,not_above(top,top),not_above(f1,top),not_above(f1,f1),not_above(bottom,top),not_above(bottom,f1),not_above(bottom,bottom)],[pinup,pinup(p5)],[not_pinup,not_pinup(p1),not_pinup(p2),not_pinup(p3),not_pinup(p4),not_pinup(p6)],[pindown,pindown(p6)],[not_pindown,not_pindown(p1),not_pindown(p2),not_pindown(p3),not_pindown(p4),not_pindown(p5)],[up],[not_up,not_up],[eq,eq(p1,p1),eq(p2,p2),eq(p3,p3),eq(p4,p4),eq(p5,p5),eq(p6,p6),eq(top,top),eq(f1,f1),eq(bottom,bottom),eq(a,a),eq(a1,a1)],[not_eq,not_eq(p1,p2),not_eq(p1,p3),not_eq(p1,p4),not_eq(p1,p5),not_eq(p1,p6),not_eq(p2,p1),not_eq(p2,p3),not_eq(p2,p4),not_eq(p2,p5),not_eq(p2,p6),not_eq(p3,p1),not_eq(p3,p2),not_eq(p3,p4),not_eq(p3,p5),not_eq(p3,p6),not_eq(p4,p1),not_eq(p4,p2),not_eq(p4,p3),not_eq(p4,p5),not_eq(p4,p6),not_eq(p5,p1),not_eq(p5,p2),not_eq(p5,p3),not_eq(p5,p4),not_eq(p5,p6),not_eq(p6,p1),not_eq(p6,p2),not_eq(p6,p3),not_eq(p6,p4),not_eq(p6,p5),not_eq(top,f1),not_eq(top,bottom),not_eq(f1,top),not_eq(f1,bottom),not_eq(bottom,top),not_eq(bottom,f1),not_eq(a,a1),not_eq(a1,a)]],[[at,at(f1)],[not_at,not_at(top),not_at(bottom)],[pup,pup(p1,bottom),pup(p2,f1)],[not_pup,not_pup(p1,top),not_pup(p1,f1),not_pup(p2,top),not_pup(p2,bottom),not_pup(p3,top),not_pup(p3,f1),not_pup(p3,bottom),not_pup(p4,top),not_pup(p4,f1),not_pup(p4,bottom),not_pup(p5,top),not_pup(p5,f1),not_pup(p5,bottom),not_pup(p6,top),not_pup(p6,f1),not_pup(p6,bottom)],[pdown,pdown(p4,top)],[not_pdown,not_pdown(p1,top),not_pdown(p1,f1),not_pdown(p1,bottom),not_pdown(p2,top),not_pdown(p2,f1),not_pdown(p2,bottom),not_pdown(p3,top),not_pdown(p3,f1),not_pdown(p3,bottom),not_pdown(p4,f1),not_pdown(p4,bottom),not_pdown(p5,top),not_pdown(p5,f1),not_pdown(p5,bottom),not_pdown(p6,top),not_pdown(p6,f1),not_pdown(p6,bottom)],[above,above(top,bottom),above(top,f1),above(f1,bottom)],[not_above,not_above(top,top),not_above(f1,top),not_above(f1,f1),not_above(bottom,top),not_above(bottom,f1),not_above(bottom,bottom)],[pinup],[not_pinup,not_pinup(p1),not_pinup(p2),not_pinup(p3),not_pinup(p4),not_pinup(p5),not_pinup(p6)],[pindown],[not_pindown,not_pindown(p1),not_pindown(p2),not_pindown(p3),not_pindown(p4),not_pindown(p5),not_pindown(p6)],[up],[not_up,not_up],[eq,eq(p1,p1),eq(p2,p2),eq(p3,p3),eq(p4,p4),eq(p5,p5),eq(p6,p6),eq(top,top),eq(f1,f1),eq(bottom,bottom),eq(a,a),eq(a1,a1)],[not_eq,not_eq(p1,p2),not_eq(p1,p3),not_eq(p1,p4),not_eq(p1,p5),not_eq(p1,p6),not_eq(p2,p1),not_eq(p2,p3),not_eq(p2,p4),not_eq(p2,p5),not_eq(p2,p6),not_eq(p3,p1),not_eq(p3,p2),not_eq(p3,p4),not_eq(p3,p5),not_eq(p3,p6),not_eq(p4,p1),not_eq(p4,p2),not_eq(p4,p3),not_eq(p4,p5),not_eq(p4,p6),not_eq(p5,p1),not_eq(p5,p2),not_eq(p5,p3),not_eq(p5,p4),not_eq(p5,p6),not_eq(p6,p1),not_eq(p6,p2),not_eq(p6,p3),not_eq(p6,p4),not_eq(p6,p5),not_eq(top,f1),not_eq(top,bottom),not_eq(f1,top),not_eq(f1,bottom),not_eq(bottom,top),not_eq(bottom,f1),not_eq(a,a1),not_eq(a1,a)]],[[at,at(bottom)],[not_at,not_at(top),not_at(f1)],[pup],[not_pup,not_pup(p1,top),not_pup(p1,f1),not_pup(p1,bottom),not_pup(p2,top),not_pup(p2,f1),not_pup(p2,bottom),not_pup(p3,top),not_pup(p3,f1),not_pup(p3,bottom),not_pup(p4,top),not_pup(p4,f1),not_pup(p4,bottom),not_pup(p5,top),not_pup(p5,f1),not_pup(p5,bottom),not_pup(p6,top),not_pup(p6,f1),not_pup(p6,bottom)],[pdown,pdown(p3,f1),pdown(p4,top)],[not_pdown,not_pdown(p1,top),not_pdown(p1,f1),not_pdown(p1,bottom),not_pdown(p2,top),not_pdown(p2,f1),not_pdown(p2,bottom),not_pdown(p3,top),not_pdown(p3,bottom),not_pdown(p4,f1),not_pdown(p4,bottom),not_pdown(p5,top),not_pdown(p5,f1),not_pdown(p5,bottom),not_pdown(p6,top),not_pdown(p6,f1),not_pdown(p6,bottom)],[above,above(top,bottom),above(top,f1),above(f1,bottom)],[not_above,not_above(top,top),not_above(f1,top),not_above(f1,f1),not_above(bottom,top),not_above(bottom,f1),not_above(bottom,bottom)],[pinup],[not_pinup,not_pinup(p1),not_pinup(p2),not_pinup(p3),not_pinup(p4),not_pinup(p5),not_pinup(p6)],[pindown,pindown(p6)],[not_pindown,not_pindown(p1),not_pindown(p2),not_pindown(p3),not_pindown(p4),not_pindown(p5)],[up],[not_up,not_up],[eq,eq(p1,p1),eq(p2,p2),eq(p3,p3),eq(p4,p4),eq(p5,p5),eq(p6,p6),eq(top,top),eq(f1,f1),eq(bottom,bottom),eq(a,a),eq(a1,a1)],[not_eq,not_eq(p1,p2),not_eq(p1,p3),not_eq(p1,p4),not_eq(p1,p5),not_eq(p1,p6),not_eq(p2,p1),not_eq(p2,p3),not_eq(p2,p4),not_eq(p2,p5),not_eq(p2,p6),not_eq(p3,p1),not_eq(p3,p2),not_eq(p3,p4),not_eq(p3,p5),not_eq(p3,p6),not_eq(p4,p1),not_eq(p4,p2),not_eq(p4,p3),not_eq(p4,p5),not_eq(p4,p6),not_eq(p5,p1),not_eq(p5,p2),not_eq(p5,p3),not_eq(p5,p4),not_eq(p5,p6),not_eq(p6,p1),not_eq(p6,p2),not_eq(p6,p3),not_eq(p6,p4),not_eq(p6,p5),not_eq(top,f1),not_eq(top,bottom),not_eq(f1,top),not_eq(f1,bottom),not_eq(bottom,top),not_eq(bottom,f1),not_eq(a,a1),not_eq(a1,a)]],[[at,at(top)],[not_at,not_at(f1),not_at(bottom)],[pup],[not_pup,not_pup(p1,top),not_pup(p1,f1),not_pup(p1,bottom),not_pup(p2,top),not_pup(p2,f1),not_pup(p2,bottom),not_pup(p3,top),not_pup(p3,f1),not_pup(p3,bottom),not_pup(p4,top),not_pup(p4,f1),not_pup(p4,bottom),not_pup(p5,top),not_pup(p5,f1),not_pup(p5,bottom),not_pup(p6,top),not_pup(p6,f1),not_pup(p6,bottom)],[pdown,pdown(p4,top)],[not_pdown,not_pdown(p1,top),not_pdown(p1,f1),not_pdown(p1,bottom),not_pdown(p2,top),not_pdown(p2,f1),not_pdown(p2,bottom),not_pdown(p3,top),not_pdown(p3,f1),not_pdown(p3,bottom),not_pdown(p4,f1),not_pdown(p4,bottom),not_pdown(p5,top),not_pdown(p5,f1),not_pdown(p5,bottom),not_pdown(p6,top),not_pdown(p6,f1),not_pdown(p6,bottom)],[above,above(top,bottom),above(top,f1),above(f1,bottom)],[not_above,not_above(top,top),not_above(f1,top),not_above(f1,f1),not_above(bottom,top),not_above(bottom,f1),not_above(bottom,bottom)],[pinup,pinup(p5)],[not_pinup,not_pinup(p1),not_pinup(p2),not_pinup(p3),not_pinup(p4),not_pinup(p6)],[pindown],[not_pindown,not_pindown(p1),not_pindown(p2),not_pindown(p3),not_pindown(p4),not_pindown(p5),not_pindown(p6)],[up],[not_up,not_up],[eq,eq(p1,p1),eq(p2,p2),eq(p3,p3),eq(p4,p4),eq(p5,p5),eq(p6,p6),eq(top,top),eq(f1,f1),eq(bottom,bottom),eq(a,a),eq(a1,a1)],[not_eq,not_eq(p1,p2),not_eq(p1,p3),not_eq(p1,p4),not_eq(p1,p5),not_eq(p1,p6),not_eq(p2,p1),not_eq(p2,p3),not_eq(p2,p4),not_eq(p2,p5),not_eq(p2,p6),not_eq(p3,p1),not_eq(p3,p2),not_eq(p3,p4),not_eq(p3,p5),not_eq(p3,p6),not_eq(p4,p1),not_eq(p4,p2),not_eq(p4,p3),not_eq(p4,p5),not_eq(p4,p6),not_eq(p5,p1),not_eq(p5,p2),not_eq(p5,p3),not_eq(p5,p4),not_eq(p5,p6),not_eq(p6,p1),not_eq(p6,p2),not_eq(p6,p3),not_eq(p6,p4),not_eq(p6,p5),not_eq(top,f1),not_eq(top,bottom),not_eq(f1,top),not_eq(f1,bottom),not_eq(bottom,top),not_eq(bottom,f1),not_eq(a,a1),not_eq(a1,a)]],[[at,at(top)],[not_at,not_at(f1),not_at(bottom)],[pup,pup(p1,bottom)],[not_pup,not_pup(p1,top),not_pup(p1,f1),not_pup(p2,top),not_pup(p2,f1),not_pup(p2,bottom),not_pup(p3,top),not_pup(p3,f1),not_pup(p3,bottom),not_pup(p4,top),not_pup(p4,f1),not_pup(p4,bottom),not_pup(p5,top),not_pup(p5,f1),not_pup(p5,bottom),not_pup(p6,top),not_pup(p6,f1),not_pup(p6,bottom)],[pdown,pdown(p3,f1),pdown(p4,top)],[not_pdown,not_pdown(p1,top),not_pdown(p1,f1),not_pdown(p1,bottom),not_pdown(p2,top),not_pdown(p2,f1),not_pdown(p2,bottom),not_pdown(p3,top),not_pdown(p3,bottom),not_pdown(p4,f1),not_pdown(p4,bottom),not_pdown(p5,top),not_pdown(p5,f1),not_pdown(p5,bottom),not_pdown(p6,top),not_pdown(p6,f1),not_pdown(p6,bottom)],[above,above(top,bottom),above(top,f1),above(f1,bottom)],[not_above,not_above(top,top),not_above(f1,top),not_above(f1,f1),not_above(bottom,top),not_above(bottom,f1),not_above(bottom,bottom)],[pinup],[not_pinup,not_pinup(p1),not_pinup(p2),not_pinup(p3),not_pinup(p4),not_pinup(p5),not_pinup(p6)],[pindown,pindown(p6)],[not_pindown,not_pindown(p1),not_pindown(p2),not_pindown(p3),not_pindown(p4),not_pindown(p5)],[up],[not_up,not_up],[eq,eq(p1,p1),eq(p2,p2),eq(p3,p3),eq(p4,p4),eq(p5,p5),eq(p6,p6),eq(top,top),eq(f1,f1),eq(bottom,bottom),eq(a,a),eq(a1,a1)],[not_eq,not_eq(p1,p2),not_eq(p1,p3),not_eq(p1,p4),not_eq(p1,p5),not_eq(p1,p6),not_eq(p2,p1),not_eq(p2,p3),not_eq(p2,p4),not_eq(p2,p5),not_eq(p2,p6),not_eq(p3,p1),not_eq(p3,p2),not_eq(p3,p4),not_eq(p3,p5),not_eq(p3,p6),not_eq(p4,p1),not_eq(p4,p2),not_eq(p4,p3),not_eq(p4,p5),not_eq(p4,p6),not_eq(p5,p1),not_eq(p5,p2),not_eq(p5,p3),not_eq(p5,p4),not_eq(p5,p6),not_eq(p6,p1),not_eq(p6,p2),not_eq(p6,p3),not_eq(p6,p4),not_eq(p6,p5),not_eq(top,f1),not_eq(top,bottom),not_eq(f1,top),not_eq(f1,bottom),not_eq(bottom,top),not_eq(bottom,f1),not_eq(a,a1),not_eq(a1,a)]],[[at,at(bottom)],[not_at,not_at(top),not_at(f1)],[pup,pup(p1,bottom),pup(p2,f1)],[not_pup,not_pup(p1,top),not_pup(p1,f1),not_pup(p2,top),not_pup(p2,bottom),not_pup(p3,top),not_pup(p3,f1),not_pup(p3,bottom),not_pup(p4,top),not_pup(p4,f1),not_pup(p4,bottom),not_pup(p5,top),not_pup(p5,f1),not_pup(p5,bottom),not_pup(p6,top),not_pup(p6,f1),not_pup(p6,bottom)],[pdown],[not_pdown,not_pdown(p1,top),not_pdown(p1,f1),not_pdown(p1,bottom),not_pdown(p2,top),not_pdown(p2,f1),not_pdown(p2,bottom),not_pdown(p3,top),not_pdown(p3,f1),not_pdown(p3,bottom),not_pdown(p4,top),not_pdown(p4,f1),not_pdown(p4,bottom),not_pdown(p5,top),not_pdown(p5,f1),not_pdown(p5,bottom),not_pdown(p6,top),not_pdown(p6,f1),not_pdown(p6,bottom)],[above,above(top,bottom),above(top,f1),above(f1,bottom)],[not_above,not_above(top,top),not_above(f1,top),not_above(f1,f1),not_above(bottom,top),not_above(bottom,f1),not_above(bottom,bottom)],[pinup],[not_pinup,not_pinup(p1),not_pinup(p2),not_pinup(p3),not_pinup(p4),not_pinup(p5),not_pinup(p6)],[pindown],[not_pindown,not_pindown(p1),not_pindown(p2),not_pindown(p3),not_pindown(p4),not_pindown(p5),not_pindown(p6)],[up],[not_up,not_up],[eq,eq(p1,p1),eq(p2,p2),eq(p3,p3),eq(p4,p4),eq(p5,p5),eq(p6,p6),eq(top,top),eq(f1,f1),eq(bottom,bottom),eq(a,a),eq(a1,a1)],[not_eq,not_eq(p1,p2),not_eq(p1,p3),not_eq(p1,p4),not_eq(p1,p5),not_eq(p1,p6),not_eq(p2,p1),not_eq(p2,p3),not_eq(p2,p4),not_eq(p2,p5),not_eq(p2,p6),not_eq(p3,p1),not_eq(p3,p2),not_eq(p3,p4),not_eq(p3,p5),not_eq(p3,p6),not_eq(p4,p1),not_eq(p4,p2),not_eq(p4,p3),not_eq(p4,p5),not_eq(p4,p6),not_eq(p5,p1),not_eq(p5,p2),not_eq(p5,p3),not_eq(p5,p4),not_eq(p5,p6),not_eq(p6,p1),not_eq(p6,p2),not_eq(p6,p3),not_eq(p6,p4),not_eq(p6,p5),not_eq(top,f1),not_eq(top,bottom),not_eq(f1,top),not_eq(f1,bottom),not_eq(bottom,top),not_eq(bottom,f1),not_eq(a,a1),not_eq(a1,a)]],[[at,at(bottom)],[not_at,not_at(top),not_at(f1)],[pup],[not_pup,not_pup(p1,top),not_pup(p1,f1),not_pup(p1,bottom),not_pup(p2,top),not_pup(p2,f1),not_pup(p2,bottom),not_pup(p3,top),not_pup(p3,f1),not_pup(p3,bottom),not_pup(p4,top),not_pup(p4,f1),not_pup(p4,bottom),not_pup(p5,top),not_pup(p5,f1),not_pup(p5,bottom),not_pup(p6,top),not_pup(p6,f1),not_pup(p6,bottom)],[pdown,pdown(p3,f1),pdown(p4,top)],[not_pdown,not_pdown(p1,top),not_pdown(p1,f1),not_pdown(p1,bottom),not_pdown(p2,top),not_pdown(p2,f1),not_pdown(p2,bottom),not_pdown(p3,top),not_pdown(p3,bottom),not_pdown(p4,f1),not_pdown(p4,bottom),not_pdown(p5,top),not_pdown(p5,f1),not_pdown(p5,bottom),not_pdown(p6,top),not_pdown(p6,f1),not_pdown(p6,bottom)],[above,above(top,bottom),above(top,f1),above(f1,bottom)],[not_above,not_above(top,top),not_above(f1,top),not_above(f1,f1),not_above(bottom,top),not_above(bottom,f1),not_above(bottom,bottom)],[pinup,pinup(p5)],[not_pinup,not_pinup(p1),not_pinup(p2),not_pinup(p3),not_pinup(p4),not_pinup(p6)],[pindown,pindown(p6)],[not_pindown,not_pindown(p1),not_pindown(p2),not_pindown(p3),not_pindown(p4),not_pindown(p5)],[up],[not_up,not_up],[eq,eq(p1,p1),eq(p2,p2),eq(p3,p3),eq(p4,p4),eq(p5,p5),eq(p6,p6),eq(top,top),eq(f1,f1),eq(bottom,bottom),eq(a,a),eq(a1,a1)],[not_eq,not_eq(p1,p2),not_eq(p1,p3),not_eq(p1,p4),not_eq(p1,p5),not_eq(p1,p6),not_eq(p2,p1),not_eq(p2,p3),not_eq(p2,p4),not_eq(p2,p5),not_eq(p2,p6),not_eq(p3,p1),not_eq(p3,p2),not_eq(p3,p4),not_eq(p3,p5),not_eq(p3,p6),not_eq(p4,p1),not_eq(p4,p2),not_eq(p4,p3),not_eq(p4,p5),not_eq(p4,p6),not_eq(p5,p1),not_eq(p5,p2),not_eq(p5,p3),not_eq(p5,p4),not_eq(p5,p6),not_eq(p6,p1),not_eq(p6,p2),not_eq(p6,p3),not_eq(p6,p4),not_eq(p6,p5),not_eq(top,f1),not_eq(top,bottom),not_eq(f1,top),not_eq(f1,bottom),not_eq(bottom,top),not_eq(bottom,f1),not_eq(a,a1),not_eq(a1,a)]],[[at,at(top)],[not_at,not_at(f1),not_at(bottom)],[pup],[not_pup,not_pup(p1,top),not_pup(p1,f1),not_pup(p1,bottom),not_pup(p2,top),not_pup(p2,f1),not_pup(p2,bottom),not_pup(p3,top),not_pup(p3,f1),not_pup(p3,bottom),not_pup(p4,top),not_pup(p4,f1),not_pup(p4,bottom),not_pup(p5,top),not_pup(p5,f1),not_pup(p5,bottom),not_pup(p6,top),not_pup(p6,f1),not_pup(p6,bottom)],[pdown,pdown(p3,f1)],[not_pdown,not_pdown(p1,top),not_pdown(p1,f1),not_pdown(p1,bottom),not_pdown(p2,top),not_pdown(p2,f1),not_pdown(p2,bottom),not_pdown(p3,top),not_pdown(p3,bottom),not_pdown(p4,top),not_pdown(p4,f1),not_pdown(p4,bottom),not_pdown(p5,top),not_pdown(p5,f1),not_pdown(p5,bottom),not_pdown(p6,top),not_pdown(p6,f1),not_pdown(p6,bottom)],[above,above(top,bottom),above(top,f1),above(f1,bottom)],[not_above,not_above(top,top),not_above(f1,top),not_above(f1,f1),not_above(bottom,top),not_above(bottom,f1),not_above(bottom,bottom)],[pinup],[not_pinup,not_pinup(p1),not_pinup(p2),not_pinup(p3),not_pinup(p4),not_pinup(p5),not_pinup(p6)],[pindown,pindown(p6)],[not_pindown,not_pindown(p1),not_pindown(p2),not_pindown(p3),not_pindown(p4),not_pindown(p5)],[up],[not_up,not_up],[eq,eq(p1,p1),eq(p2,p2),eq(p3,p3),eq(p4,p4),eq(p5,p5),eq(p6,p6),eq(top,top),eq(f1,f1),eq(bottom,bottom),eq(a,a),eq(a1,a1)],[not_eq,not_eq(p1,p2),not_eq(p1,p3),not_eq(p1,p4),not_eq(p1,p5),not_eq(p1,p6),not_eq(p2,p1),not_eq(p2,p3),not_eq(p2,p4),not_eq(p2,p5),not_eq(p2,p6),not_eq(p3,p1),not_eq(p3,p2),not_eq(p3,p4),not_eq(p3,p5),not_eq(p3,p6),not_eq(p4,p1),not_eq(p4,p2),not_eq(p4,p3),not_eq(p4,p5),not_eq(p4,p6),not_eq(p5,p1),not_eq(p5,p2),not_eq(p5,p3),not_eq(p5,p4),not_eq(p5,p6),not_eq(p6,p1),not_eq(p6,p2),not_eq(p6,p3),not_eq(p6,p4),not_eq(p6,p5),not_eq(top,f1),not_eq(top,bottom),not_eq(f1,top),not_eq(f1,bottom),not_eq(bottom,top),not_eq(bottom,f1),not_eq(a,a1),not_eq(a1,a)]],[[at,at(f1)],[not_at,not_at(top),not_at(bottom)],[pup,pup(p1,bottom)],[not_pup,not_pup(p1,top),not_pup(p1,f1),not_pup(p2,top),not_pup(p2,f1),not_pup(p2,bottom),not_pup(p3,top),not_pup(p3,f1),not_pup(p3,bottom),not_pup(p4,top),not_pup(p4,f1),not_pup(p4,bottom),not_pup(p5,top),not_pup(p5,f1),not_pup(p5,bottom),not_pup(p6,top),not_pup(p6,f1),not_pup(p6,bottom)],[pdown,pdown(p3,f1),pdown(p4,top)],[not_pdown,not_pdown(p1,top),not_pdown(p1,f1),not_pdown(p1,bottom),not_pdown(p2,top),not_pdown(p2,f1),not_pdown(p2,bottom),not_pdown(p3,top),not_pdown(p3,bottom),not_pdown(p4,f1),not_pdown(p4,bottom),not_pdown(p5,top),not_pdown(p5,f1),not_pdown(p5,bottom),not_pdown(p6,top),not_pdown(p6,f1),not_pdown(p6,bottom)],[above,above(top,bottom),above(top,f1),above(f1,bottom)],[not_above,not_above(top,top),not_above(f1,top),not_above(f1,f1),not_above(bottom,top),not_above(bottom,f1),not_above(bottom,bottom)],[pinup,pinup(p5)],[not_pinup,not_pinup(p1),not_pinup(p2),not_pinup(p3),not_pinup(p4),not_pinup(p6)],[pindown],[not_pindown,not_pindown(p1),not_pindown(p2),not_pindown(p3),not_pindown(p4),not_pindown(p5),not_pindown(p6)],[up],[not_up,not_up],[eq,eq(p1,p1),eq(p2,p2),eq(p3,p3),eq(p4,p4),eq(p5,p5),eq(p6,p6),eq(top,top),eq(f1,f1),eq(bottom,bottom),eq(a,a),eq(a1,a1)],[not_eq,not_eq(p1,p2),not_eq(p1,p3),not_eq(p1,p4),not_eq(p1,p5),not_eq(p1,p6),not_eq(p2,p1),not_eq(p2,p3),not_eq(p2,p4),not_eq(p2,p5),not_eq(p2,p6),not_eq(p3,p1),not_eq(p3,p2),not_eq(p3,p4),not_eq(p3,p5),not_eq(p3,p6),not_eq(p4,p1),not_eq(p4,p2),not_eq(p4,p3),not_eq(p4,p5),not_eq(p4,p6),not_eq(p5,p1),not_eq(p5,p2),not_eq(p5,p3),not_eq(p5,p4),not_eq(p5,p6),not_eq(p6,p1),not_eq(p6,p2),not_eq(p6,p3),not_eq(p6,p4),not_eq(p6,p5),not_eq(top,f1),not_eq(top,bottom),not_eq(f1,top),not_eq(f1,bottom),not_eq(bottom,top),not_eq(bottom,f1),not_eq(a,a1),not_eq(a1,a)]],[[at,at(f1)],[not_at,not_at(top),not_at(bottom)],[pup,pup(p1,bottom),pup(p2,f1)],[not_pup,not_pup(p1,top),not_pup(p1,f1),not_pup(p2,top),not_pup(p2,bottom),not_pup(p3,top),not_pup(p3,f1),not_pup(p3,bottom),not_pup(p4,top),not_pup(p4,f1),not_pup(p4,bottom),not_pup(p5,top),not_pup(p5,f1),not_pup(p5,bottom),not_pup(p6,top),not_pup(p6,f1),not_pup(p6,bottom)],[pdown,pdown(p3,f1),pdown(p4,top)],[not_pdown,not_pdown(p1,top),not_pdown(p1,f1),not_pdown(p1,bottom),not_pdown(p2,top),not_pdown(p2,f1),not_pdown(p2,bottom),not_pdown(p3,top),not_pdown(p3,bottom),not_pdown(p4,f1),not_pdown(p4,bottom),not_pdown(p5,top),not_pdown(p5,f1),not_pdown(p5,bottom),not_pdown(p6,top),not_pdown(p6,f1),not_pdown(p6,bottom)],[above,above(top,bottom),above(top,f1),above(f1,bottom)],[not_above,not_above(top,top),not_above(f1,top),not_above(f1,f1),not_above(bottom,top),not_above(bottom,f1),not_above(bottom,bottom)],[pinup],[not_pinup,not_pinup(p1),not_pinup(p2),not_pinup(p3),not_pinup(p4),not_pinup(p5),not_pinup(p6)],[pindown],[not_pindown,not_pindown(p1),not_pindown(p2),not_pindown(p3),not_pindown(p4),not_pindown(p5),not_pindown(p6)],[up],[not_up,not_up],[eq,eq(p1,p1),eq(p2,p2),eq(p3,p3),eq(p4,p4),eq(p5,p5),eq(p6,p6),eq(top,top),eq(f1,f1),eq(bottom,bottom),eq(a,a),eq(a1,a1)],[not_eq,not_eq(p1,p2),not_eq(p1,p3),not_eq(p1,p4),not_eq(p1,p5),not_eq(p1,p6),not_eq(p2,p1),not_eq(p2,p3),not_eq(p2,p4),not_eq(p2,p5),not_eq(p2,p6),not_eq(p3,p1),not_eq(p3,p2),not_eq(p3,p4),not_eq(p3,p5),not_eq(p3,p6),not_eq(p4,p1),not_eq(p4,p2),not_eq(p4,p3),not_eq(p4,p5),not_eq(p4,p6),not_eq(p5,p1),not_eq(p5,p2),not_eq(p5,p3),not_eq(p5,p4),not_eq(p5,p6),not_eq(p6,p1),not_eq(p6,p2),not_eq(p6,p3),not_eq(p6,p4),not_eq(p6,p5),not_eq(top,f1),not_eq(top,bottom),not_eq(f1,top),not_eq(f1,bottom),not_eq(bottom,top),not_eq(bottom,f1),not_eq(a,a1),not_eq(a1,a)]],[[at,at(bottom)],[not_at,not_at(top),not_at(f1)],[pup,pup(p1,bottom),pup(p2,f1)],[not_pup,not_pup(p1,top),not_pup(p1,f1),not_pup(p2,top),not_pup(p2,bottom),not_pup(p3,top),not_pup(p3,f1),not_pup(p3,bottom),not_pup(p4,top),not_pup(p4,f1),not_pup(p4,bottom),not_pup(p5,top),not_pup(p5,f1),not_pup(p5,bottom),not_pup(p6,top),not_pup(p6,f1),not_pup(p6,bottom)],[pdown],[not_pdown,not_pdown(p1,top),not_pdown(p1,f1),not_pdown(p1,bottom),not_pdown(p2,top),not_pdown(p2,f1),not_pdown(p2,bottom),not_pdown(p3,top),not_pdown(p3,f1),not_pdown(p3,bottom),not_pdown(p4,top),not_pdown(p4,f1),not_pdown(p4,bottom),not_pdown(p5,top),not_pdown(p5,f1),not_pdown(p5,bottom),not_pdown(p6,top),not_pdown(p6,f1),not_pdown(p6,bottom)],[above,above(top,bottom),above(top,f1),above(f1,bottom)],[not_above,not_above(top,top),not_above(f1,top),not_above(f1,f1),not_above(bottom,top),not_above(bottom,f1),not_above(bottom,bottom)],[pinup,pinup(p5)],[not_pinup,not_pinup(p1),not_pinup(p2),not_pinup(p3),not_pinup(p4),not_pinup(p6)],[pindown],[not_pindown,not_pindown(p1),not_pindown(p2),not_pindown(p3),not_pindown(p4),not_pindown(p5),not_pindown(p6)],[up],[not_up,not_up],[eq,eq(p1,p1),eq(p2,p2),eq(p3,p3),eq(p4,p4),eq(p5,p5),eq(p6,p6),eq(top,top),eq(f1,f1),eq(bottom,bottom),eq(a,a),eq(a1,a1)],[not_eq,not_eq(p1,p2),not_eq(p1,p3),not_eq(p1,p4),not_eq(p1,p5),not_eq(p1,p6),not_eq(p2,p1),not_eq(p2,p3),not_eq(p2,p4),not_eq(p2,p5),not_eq(p2,p6),not_eq(p3,p1),not_eq(p3,p2),not_eq(p3,p4),not_eq(p3,p5),not_eq(p3,p6),not_eq(p4,p1),not_eq(p4,p2),not_eq(p4,p3),not_eq(p4,p5),not_eq(p4,p6),not_eq(p5,p1),not_eq(p5,p2),not_eq(p5,p3),not_eq(p5,p4),not_eq(p5,p6),not_eq(p6,p1),not_eq(p6,p2),not_eq(p6,p3),not_eq(p6,p4),not_eq(p6,p5),not_eq(top,f1),not_eq(top,bottom),not_eq(f1,top),not_eq(f1,bottom),not_eq(bottom,top),not_eq(bottom,f1),not_eq(a,a1),not_eq(a1,a)]],[[at,at(bottom)],[not_at,not_at(top),not_at(f1)],[pup,pup(p1,bottom)],[not_pup,not_pup(p1,top),not_pup(p1,f1),not_pup(p2,top),not_pup(p2,f1),not_pup(p2,bottom),not_pup(p3,top),not_pup(p3,f1),not_pup(p3,bottom),not_pup(p4,top),not_pup(p4,f1),not_pup(p4,bottom),not_pup(p5,top),not_pup(p5,f1),not_pup(p5,bottom),not_pup(p6,top),not_pup(p6,f1),not_pup(p6,bottom)],[pdown],[not_pdown,not_pdown(p1,top),not_pdown(p1,f1),not_pdown(p1,bottom),not_pdown(p2,top),not_pdown(p2,f1),not_pdown(p2,bottom),not_pdown(p3,top),not_pdown(p3,f1),not_pdown(p3,bottom),not_pdown(p4,top),not_pdown(p4,f1),not_pdown(p4,bottom),not_pdown(p5,top),not_pdown(p5,f1),not_pdown(p5,bottom),not_pdown(p6,top),not_pdown(p6,f1),not_pdown(p6,bottom)],[above,above(top,bottom),above(top,f1),above(f1,bottom)],[not_above,not_above(top,top),not_above(f1,top),not_above(f1,f1),not_above(bottom,top),not_above(bottom,f1),not_above(bottom,bottom)],[pinup,pinup(p5)],[not_pinup,not_pinup(p1),not_pinup(p2),not_pinup(p3),not_pinup(p4),not_pinup(p6)],[pindown],[not_pindown,not_pindown(p1),not_pindown(p2),not_pindown(p3),not_pindown(p4),not_pindown(p5),not_pindown(p6)],[up],[not_up,not_up],[eq,eq(p1,p1),eq(p2,p2),eq(p3,p3),eq(p4,p4),eq(p5,p5),eq(p6,p6),eq(top,top),eq(f1,f1),eq(bottom,bottom),eq(a,a),eq(a1,a1)],[not_eq,not_eq(p1,p2),not_eq(p1,p3),not_eq(p1,p4),not_eq(p1,p5),not_eq(p1,p6),not_eq(p2,p1),not_eq(p2,p3),not_eq(p2,p4),not_eq(p2,p5),not_eq(p2,p6),not_eq(p3,p1),not_eq(p3,p2),not_eq(p3,p4),not_eq(p3,p5),not_eq(p3,p6),not_eq(p4,p1),not_eq(p4,p2),not_eq(p4,p3),not_eq(p4,p5),not_eq(p4,p6),not_eq(p5,p1),not_eq(p5,p2),not_eq(p5,p3),not_eq(p5,p4),not_eq(p5,p6),not_eq(p6,p1),not_eq(p6,p2),not_eq(p6,p3),not_eq(p6,p4),not_eq(p6,p5),not_eq(top,f1),not_eq(top,bottom),not_eq(f1,top),not_eq(f1,bottom),not_eq(bottom,top),not_eq(bottom,f1),not_eq(a,a1),not_eq(a1,a)]],[[at,at(f1)],[not_at,not_at(top),not_at(bottom)],[pup,pup(p1,bottom),pup(p2,f1)],[not_pup,not_pup(p1,top),not_pup(p1,f1),not_pup(p2,top),not_pup(p2,bottom),not_pup(p3,top),not_pup(p3,f1),not_pup(p3,bottom),not_pup(p4,top),not_pup(p4,f1),not_pup(p4,bottom),not_pup(p5,top),not_pup(p5,f1),not_pup(p5,bottom),not_pup(p6,top),not_pup(p6,f1),not_pup(p6,bottom)],[pdown],[not_pdown,not_pdown(p1,top),not_pdown(p1,f1),not_pdown(p1,bottom),not_pdown(p2,top),not_pdown(p2,f1),not_pdown(p2,bottom),not_pdown(p3,top),not_pdown(p3,f1),not_pdown(p3,bottom),not_pdown(p4,top),not_pdown(p4,f1),not_pdown(p4,bottom),not_pdown(p5,top),not_pdown(p5,f1),not_pdown(p5,bottom),not_pdown(p6,top),not_pdown(p6,f1),not_pdown(p6,bottom)],[above,above(top,bottom),above(top,f1),above(f1,bottom)],[not_above,not_above(top,top),not_above(f1,top),not_above(f1,f1),not_above(bottom,top),not_above(bottom,f1),not_above(bottom,bottom)],[pinup,pinup(p5)],[not_pinup,not_pinup(p1),not_pinup(p2),not_pinup(p3),not_pinup(p4),not_pinup(p6)],[pindown],[not_pindown,not_pindown(p1),not_pindown(p2),not_pindown(p3),not_pindown(p4),not_pindown(p5),not_pindown(p6)],[up],[not_up,not_up],[eq,eq(p1,p1),eq(p2,p2),eq(p3,p3),eq(p4,p4),eq(p5,p5),eq(p6,p6),eq(top,top),eq(f1,f1),eq(bottom,bottom),eq(a,a),eq(a1,a1)],[not_eq,not_eq(p1,p2),not_eq(p1,p3),not_eq(p1,p4),not_eq(p1,p5),not_eq(p1,p6),not_eq(p2,p1),not_eq(p2,p3),not_eq(p2,p4),not_eq(p2,p5),not_eq(p2,p6),not_eq(p3,p1),not_eq(p3,p2),not_eq(p3,p4),not_eq(p3,p5),not_eq(p3,p6),not_eq(p4,p1),not_eq(p4,p2),not_eq(p4,p3),not_eq(p4,p5),not_eq(p4,p6),not_eq(p5,p1),not_eq(p5,p2),not_eq(p5,p3),not_eq(p5,p4),not_eq(p5,p6),not_eq(p6,p1),not_eq(p6,p2),not_eq(p6,p3),not_eq(p6,p4),not_eq(p6,p5),not_eq(top,f1),not_eq(top,bottom),not_eq(f1,top),not_eq(f1,bottom),not_eq(bottom,top),not_eq(bottom,f1),not_eq(a,a1),not_eq(a1,a)]],[[at,at(f1)],[not_at,not_at(top),not_at(bottom)],[pup,pup(p1,bottom),pup(p2,f1)],[not_pup,not_pup(p1,top),not_pup(p1,f1),not_pup(p2,top),not_pup(p2,bottom),not_pup(p3,top),not_pup(p3,f1),not_pup(p3,bottom),not_pup(p4,top),not_pup(p4,f1),not_pup(p4,bottom),not_pup(p5,top),not_pup(p5,f1),not_pup(p5,bottom),not_pup(p6,top),not_pup(p6,f1),not_pup(p6,bottom)],[pdown],[not_pdown,not_pdown(p1,top),not_pdown(p1,f1),not_pdown(p1,bottom),not_pdown(p2,top),not_pdown(p2,f1),not_pdown(p2,bottom),not_pdown(p3,top),not_pdown(p3,f1),not_pdown(p3,bottom),not_pdown(p4,top),not_pdown(p4,f1),not_pdown(p4,bottom),not_pdown(p5,top),not_pdown(p5,f1),not_pdown(p5,bottom),not_pdown(p6,top),not_pdown(p6,f1),not_pdown(p6,bottom)],[above,above(top,bottom),above(top,f1),above(f1,bottom)],[not_above,not_above(top,top),not_above(f1,top),not_above(f1,f1),not_above(bottom,top),not_above(bottom,f1),not_above(bottom,bottom)],[pinup],[not_pinup,not_pinup(p1),not_pinup(p2),not_pinup(p3),not_pinup(p4),not_pinup(p5),not_pinup(p6)],[pindown],[not_pindown,not_pindown(p1),not_pindown(p2),not_pindown(p3),not_pindown(p4),not_pindown(p5),not_pindown(p6)],[up],[not_up,not_up],[eq,eq(p1,p1),eq(p2,p2),eq(p3,p3),eq(p4,p4),eq(p5,p5),eq(p6,p6),eq(top,top),eq(f1,f1),eq(bottom,bottom),eq(a,a),eq(a1,a1)],[not_eq,not_eq(p1,p2),not_eq(p1,p3),not_eq(p1,p4),not_eq(p1,p5),not_eq(p1,p6),not_eq(p2,p1),not_eq(p2,p3),not_eq(p2,p4),not_eq(p2,p5),not_eq(p2,p6),not_eq(p3,p1),not_eq(p3,p2),not_eq(p3,p4),not_eq(p3,p5),not_eq(p3,p6),not_eq(p4,p1),not_eq(p4,p2),not_eq(p4,p3),not_eq(p4,p5),not_eq(p4,p6),not_eq(p5,p1),not_eq(p5,p2),not_eq(p5,p3),not_eq(p5,p4),not_eq(p5,p6),not_eq(p6,p1),not_eq(p6,p2),not_eq(p6,p3),not_eq(p6,p4),not_eq(p6,p5),not_eq(top,f1),not_eq(top,bottom),not_eq(f1,top),not_eq(f1,bottom),not_eq(bottom,top),not_eq(bottom,f1),not_eq(a,a1),not_eq(a1,a)]],[[at,at(bottom)],[not_at,not_at(top),not_at(f1)],[pup,pup(p1,bottom),pup(p2,f1)],[not_pup,not_pup(p1,top),not_pup(p1,f1),not_pup(p2,top),not_pup(p2,bottom),not_pup(p3,top),not_pup(p3,f1),not_pup(p3,bottom),not_pup(p4,top),not_pup(p4,f1),not_pup(p4,bottom),not_pup(p5,top),not_pup(p5,f1),not_pup(p5,bottom),not_pup(p6,top),not_pup(p6,f1),not_pup(p6,bottom)],[pdown,pdown(p4,top)],[not_pdown,not_pdown(p1,top),not_pdown(p1,f1),not_pdown(p1,bottom),not_pdown(p2,top),not_pdown(p2,f1),not_pdown(p2,bottom),not_pdown(p3,top),not_pdown(p3,f1),not_pdown(p3,bottom),not_pdown(p4,f1),not_pdown(p4,bottom),not_pdown(p5,top),not_pdown(p5,f1),not_pdown(p5,bottom),not_pdown(p6,top),not_pdown(p6,f1),not_pdown(p6,bottom)],[above,above(top,bottom),above(top,f1),above(f1,bottom)],[not_above,not_above(top,top),not_above(f1,top),not_above(f1,f1),not_above(bottom,top),not_above(bottom,f1),not_above(bottom,bottom)],[pinup],[not_pinup,not_pinup(p1),not_pinup(p2),not_pinup(p3),not_pinup(p4),not_pinup(p5),not_pinup(p6)],[pindown,pindown(p6)],[not_pindown,not_pindown(p1),not_pindown(p2),not_pindown(p3),not_pindown(p4),not_pindown(p5)],[up],[not_up,not_up],[eq,eq(p1,p1),eq(p2,p2),eq(p3,p3),eq(p4,p4),eq(p5,p5),eq(p6,p6),eq(top,top),eq(f1,f1),eq(bottom,bottom),eq(a,a),eq(a1,a1)],[not_eq,not_eq(p1,p2),not_eq(p1,p3),not_eq(p1,p4),not_eq(p1,p5),not_eq(p1,p6),not_eq(p2,p1),not_eq(p2,p3),not_eq(p2,p4),not_eq(p2,p5),not_eq(p2,p6),not_eq(p3,p1),not_eq(p3,p2),not_eq(p3,p4),not_eq(p3,p5),not_eq(p3,p6),not_eq(p4,p1),not_eq(p4,p2),not_eq(p4,p3),not_eq(p4,p5),not_eq(p4,p6),not_eq(p5,p1),not_eq(p5,p2),not_eq(p5,p3),not_eq(p5,p4),not_eq(p5,p6),not_eq(p6,p1),not_eq(p6,p2),not_eq(p6,p3),not_eq(p6,p4),not_eq(p6,p5),not_eq(top,f1),not_eq(top,bottom),not_eq(f1,top),not_eq(f1,bottom),not_eq(bottom,top),not_eq(bottom,f1),not_eq(a,a1),not_eq(a1,a)]],[[at,at(top)],[not_at,not_at(f1),not_at(bottom)],[pup,pup(p1,bottom),pup(p2,f1)],[not_pup,not_pup(p1,top),not_pup(p1,f1),not_pup(p2,top),not_pup(p2,bottom),not_pup(p3,top),not_pup(p3,f1),not_pup(p3,bottom),not_pup(p4,top),not_pup(p4,f1),not_pup(p4,bottom),not_pup(p5,top),not_pup(p5,f1),not_pup(p5,bottom),not_pup(p6,top),not_pup(p6,f1),not_pup(p6,bottom)],[pdown,pdown(p3,f1),pdown(p4,top)],[not_pdown,not_pdown(p1,top),not_pdown(p1,f1),not_pdown(p1,bottom),not_pdown(p2,top),not_pdown(p2,f1),not_pdown(p2,bottom),not_pdown(p3,top),not_pdown(p3,bottom),not_pdown(p4,f1),not_pdown(p4,bottom),not_pdown(p5,top),not_pdown(p5,f1),not_pdown(p5,bottom),not_pdown(p6,top),not_pdown(p6,f1),not_pdown(p6,bottom)],[above,above(top,bottom),above(top,f1),above(f1,bottom)],[not_above,not_above(top,top),not_above(f1,top),not_above(f1,f1),not_above(bottom,top),not_above(bottom,f1),not_above(bottom,bottom)],[pinup],[not_pinup,not_pinup(p1),not_pinup(p2),not_pinup(p3),not_pinup(p4),not_pinup(p5),not_pinup(p6)],[pindown,pindown(p6)],[not_pindown,not_pindown(p1),not_pindown(p2),not_pindown(p3),not_pindown(p4),not_pindown(p5)],[up],[not_up,not_up],[eq,eq(p1,p1),eq(p2,p2),eq(p3,p3),eq(p4,p4),eq(p5,p5),eq(p6,p6),eq(top,top),eq(f1,f1),eq(bottom,bottom),eq(a,a),eq(a1,a1)],[not_eq,not_eq(p1,p2),not_eq(p1,p3),not_eq(p1,p4),not_eq(p1,p5),not_eq(p1,p6),not_eq(p2,p1),not_eq(p2,p3),not_eq(p2,p4),not_eq(p2,p5),not_eq(p2,p6),not_eq(p3,p1),not_eq(p3,p2),not_eq(p3,p4),not_eq(p3,p5),not_eq(p3,p6),not_eq(p4,p1),not_eq(p4,p2),not_eq(p4,p3),not_eq(p4,p5),not_eq(p4,p6),not_eq(p5,p1),not_eq(p5,p2),not_eq(p5,p3),not_eq(p5,p4),not_eq(p5,p6),not_eq(p6,p1),not_eq(p6,p2),not_eq(p6,p3),not_eq(p6,p4),not_eq(p6,p5),not_eq(top,f1),not_eq(top,bottom),not_eq(f1,top),not_eq(f1,bottom),not_eq(bottom,top),not_eq(bottom,f1),not_eq(a,a1),not_eq(a1,a)]],[[at,at(f1)],[not_at,not_at(top),not_at(bottom)],[pup,pup(p2,f1)],[not_pup,not_pup(p1,top),not_pup(p1,f1),not_pup(p1,bottom),not_pup(p2,top),not_pup(p2,bottom),not_pup(p3,top),not_pup(p3,f1),not_pup(p3,bottom),not_pup(p4,top),not_pup(p4,f1),not_pup(p4,bottom),not_pup(p5,top),not_pup(p5,f1),not_pup(p5,bottom),not_pup(p6,top),not_pup(p6,f1),not_pup(p6,bottom)],[pdown,pdown(p4,top)],[not_pdown,not_pdown(p1,top),not_pdown(p1,f1),not_pdown(p1,bottom),not_pdown(p2,top),not_pdown(p2,f1),not_pdown(p2,bottom),not_pdown(p3,top),not_pdown(p3,f1),not_pdown(p3,bottom),not_pdown(p4,f1),not_pdown(p4,bottom),not_pdown(p5,top),not_pdown(p5,f1),not_pdown(p5,bottom),not_pdown(p6,top),not_pdown(p6,f1),not_pdown(p6,bottom)],[above,above(top,bottom),above(top,f1),above(f1,bottom)],[not_above,not_above(top,top),not_above(f1,top),not_above(f1,f1),not_above(bottom,top),not_above(bottom,f1),not_above(bottom,bottom)],[pinup,pinup(p5)],[not_pinup,not_pinup(p1),not_pinup(p2),not_pinup(p3),not_pinup(p4),not_pinup(p6)],[pindown,pindown(p6)],[not_pindown,not_pindown(p1),not_pindown(p2),not_pindown(p3),not_pindown(p4),not_pindown(p5)],[up],[not_up,not_up],[eq,eq(p1,p1),eq(p2,p2),eq(p3,p3),eq(p4,p4),eq(p5,p5),eq(p6,p6),eq(top,top),eq(f1,f1),eq(bottom,bottom),eq(a,a),eq(a1,a1)],[not_eq,not_eq(p1,p2),not_eq(p1,p3),not_eq(p1,p4),not_eq(p1,p5),not_eq(p1,p6),not_eq(p2,p1),not_eq(p2,p3),not_eq(p2,p4),not_eq(p2,p5),not_eq(p2,p6),not_eq(p3,p1),not_eq(p3,p2),not_eq(p3,p4),not_eq(p3,p5),not_eq(p3,p6),not_eq(p4,p1),not_eq(p4,p2),not_eq(p4,p3),not_eq(p4,p5),not_eq(p4,p6),not_eq(p5,p1),not_eq(p5,p2),not_eq(p5,p3),not_eq(p5,p4),not_eq(p5,p6),not_eq(p6,p1),not_eq(p6,p2),not_eq(p6,p3),not_eq(p6,p4),not_eq(p6,p5),not_eq(top,f1),not_eq(top,bottom),not_eq(f1,top),not_eq(f1,bottom),not_eq(bottom,top),not_eq(bottom,f1),not_eq(a,a1),not_eq(a1,a)]],[[at,at(f1)],[not_at,not_at(top),not_at(bottom)],[pup],[not_pup,not_pup(p1,top),not_pup(p1,f1),not_pup(p1,bottom),not_pup(p2,top),not_pup(p2,f1),not_pup(p2,bottom),not_pup(p3,top),not_pup(p3,f1),not_pup(p3,bottom),not_pup(p4,top),not_pup(p4,f1),not_pup(p4,bottom),not_pup(p5,top),not_pup(p5,f1),not_pup(p5,bottom),not_pup(p6,top),not_pup(p6,f1),not_pup(p6,bottom)],[pdown,pdown(p4,top)],[not_pdown,not_pdown(p1,top),not_pdown(p1,f1),not_pdown(p1,bottom),not_pdown(p2,top),not_pdown(p2,f1),not_pdown(p2,bottom),not_pdown(p3,top),not_pdown(p3,f1),not_pdown(p3,bottom),not_pdown(p4,f1),not_pdown(p4,bottom),not_pdown(p5,top),not_pdown(p5,f1),not_pdown(p5,bottom),not_pdown(p6,top),not_pdown(p6,f1),not_pdown(p6,bottom)],[above,above(top,bottom),above(top,f1),above(f1,bottom)],[not_above,not_above(top,top),not_above(f1,top),not_above(f1,f1),not_above(bottom,top),not_above(bottom,f1),not_above(bottom,bottom)],[pinup],[not_pinup,not_pinup(p1),not_pinup(p2),not_pinup(p3),not_pinup(p4),not_pinup(p5),not_pinup(p6)],[pindown,pindown(p6)],[not_pindown,not_pindown(p1),not_pindown(p2),not_pindown(p3),not_pindown(p4),not_pindown(p5)],[up],[not_up,not_up],[eq,eq(p1,p1),eq(p2,p2),eq(p3,p3),eq(p4,p4),eq(p5,p5),eq(p6,p6),eq(top,top),eq(f1,f1),eq(bottom,bottom),eq(a,a),eq(a1,a1)],[not_eq,not_eq(p1,p2),not_eq(p1,p3),not_eq(p1,p4),not_eq(p1,p5),not_eq(p1,p6),not_eq(p2,p1),not_eq(p2,p3),not_eq(p2,p4),not_eq(p2,p5),not_eq(p2,p6),not_eq(p3,p1),not_eq(p3,p2),not_eq(p3,p4),not_eq(p3,p5),not_eq(p3,p6),not_eq(p4,p1),not_eq(p4,p2),not_eq(p4,p3),not_eq(p4,p5),not_eq(p4,p6),not_eq(p5,p1),not_eq(p5,p2),not_eq(p5,p3),not_eq(p5,p4),not_eq(p5,p6),not_eq(p6,p1),not_eq(p6,p2),not_eq(p6,p3),not_eq(p6,p4),not_eq(p6,p5),not_eq(top,f1),not_eq(top,bottom),not_eq(f1,top),not_eq(f1,bottom),not_eq(bottom,top),not_eq(bottom,f1),not_eq(a,a1),not_eq(a1,a)]],[[at,at(f1)],[not_at,not_at(top),not_at(bottom)],[pup,pup(p1,bottom)],[not_pup,not_pup(p1,top),not_pup(p1,f1),not_pup(p2,top),not_pup(p2,f1),not_pup(p2,bottom),not_pup(p3,top),not_pup(p3,f1),not_pup(p3,bottom),not_pup(p4,top),not_pup(p4,f1),not_pup(p4,bottom),not_pup(p5,top),not_pup(p5,f1),not_pup(p5,bottom),not_pup(p6,top),not_pup(p6,f1),not_pup(p6,bottom)],[pdown,pdown(p4,top)],[not_pdown,not_pdown(p1,top),not_pdown(p1,f1),not_pdown(p1,bottom),not_pdown(p2,top),not_pdown(p2,f1),not_pdown(p2,bottom),not_pdown(p3,top),not_pdown(p3,f1),not_pdown(p3,bottom),not_pdown(p4,f1),not_pdown(p4,bottom),not_pdown(p5,top),not_pdown(p5,f1),not_pdown(p5,bottom),not_pdown(p6,top),not_pdown(p6,f1),not_pdown(p6,bottom)],[above,above(top,bottom),above(top,f1),above(f1,bottom)],[not_above,not_above(top,top),not_above(f1,top),not_above(f1,f1),not_above(bottom,top),not_above(bottom,f1),not_above(bottom,bottom)],[pinup],[not_pinup,not_pinup(p1),not_pinup(p2),not_pinup(p3),not_pinup(p4),not_pinup(p5),not_pinup(p6)],[pindown],[not_pindown,not_pindown(p1),not_pindown(p2),not_pindown(p3),not_pindown(p4),not_pindown(p5),not_pindown(p6)],[up],[not_up,not_up],[eq,eq(p1,p1),eq(p2,p2),eq(p3,p3),eq(p4,p4),eq(p5,p5),eq(p6,p6),eq(top,top),eq(f1,f1),eq(bottom,bottom),eq(a,a),eq(a1,a1)],[not_eq,not_eq(p1,p2),not_eq(p1,p3),not_eq(p1,p4),not_eq(p1,p5),not_eq(p1,p6),not_eq(p2,p1),not_eq(p2,p3),not_eq(p2,p4),not_eq(p2,p5),not_eq(p2,p6),not_eq(p3,p1),not_eq(p3,p2),not_eq(p3,p4),not_eq(p3,p5),not_eq(p3,p6),not_eq(p4,p1),not_eq(p4,p2),not_eq(p4,p3),not_eq(p4,p5),not_eq(p4,p6),not_eq(p5,p1),not_eq(p5,p2),not_eq(p5,p3),not_eq(p5,p4),not_eq(p5,p6),not_eq(p6,p1),not_eq(p6,p2),not_eq(p6,p3),not_eq(p6,p4),not_eq(p6,p5),not_eq(top,f1),not_eq(top,bottom),not_eq(f1,top),not_eq(f1,bottom),not_eq(bottom,top),not_eq(bottom,f1),not_eq(a,a1),not_eq(a1,a)]],[[at,at(bottom)],[not_at,not_at(top),not_at(f1)],[pup,pup(p1,bottom)],[not_pup,not_pup(p1,top),not_pup(p1,f1),not_pup(p2,top),not_pup(p2,f1),not_pup(p2,bottom),not_pup(p3,top),not_pup(p3,f1),not_pup(p3,bottom),not_pup(p4,top),not_pup(p4,f1),not_pup(p4,bottom),not_pup(p5,top),not_pup(p5,f1),not_pup(p5,bottom),not_pup(p6,top),not_pup(p6,f1),not_pup(p6,bottom)],[pdown,pdown(p3,f1)],[not_pdown,not_pdown(p1,top),not_pdown(p1,f1),not_pdown(p1,bottom),not_pdown(p2,top),not_pdown(p2,f1),not_pdown(p2,bottom),not_pdown(p3,top),not_pdown(p3,bottom),not_pdown(p4,top),not_pdown(p4,f1),not_pdown(p4,bottom),not_pdown(p5,top),not_pdown(p5,f1),not_pdown(p5,bottom),not_pdown(p6,top),not_pdown(p6,f1),not_pdown(p6,bottom)],[above,above(top,bottom),above(top,f1),above(f1,bottom)],[not_above,not_above(top,top),not_above(f1,top),not_above(f1,f1),not_above(bottom,top),not_above(bottom,f1),not_above(bottom,bottom)],[pinup,pinup(p5)],[not_pinup,not_pinup(p1),not_pinup(p2),not_pinup(p3),not_pinup(p4),not_pinup(p6)],[pindown,pindown(p6)],[not_pindown,not_pindown(p1),not_pindown(p2),not_pindown(p3),not_pindown(p4),not_pindown(p5)],[up],[not_up,not_up],[eq,eq(p1,p1),eq(p2,p2),eq(p3,p3),eq(p4,p4),eq(p5,p5),eq(p6,p6),eq(top,top),eq(f1,f1),eq(bottom,bottom),eq(a,a),eq(a1,a1)],[not_eq,not_eq(p1,p2),not_eq(p1,p3),not_eq(p1,p4),not_eq(p1,p5),not_eq(p1,p6),not_eq(p2,p1),not_eq(p2,p3),not_eq(p2,p4),not_eq(p2,p5),not_eq(p2,p6),not_eq(p3,p1),not_eq(p3,p2),not_eq(p3,p4),not_eq(p3,p5),not_eq(p3,p6),not_eq(p4,p1),not_eq(p4,p2),not_eq(p4,p3),not_eq(p4,p5),not_eq(p4,p6),not_eq(p5,p1),not_eq(p5,p2),not_eq(p5,p3),not_eq(p5,p4),not_eq(p5,p6),not_eq(p6,p1),not_eq(p6,p2),not_eq(p6,p3),not_eq(p6,p4),not_eq(p6,p5),not_eq(top,f1),not_eq(top,bottom),not_eq(f1,top),not_eq(f1,bottom),not_eq(bottom,top),not_eq(bottom,f1),not_eq(a,a1),not_eq(a1,a)]],[[at,at(f1)],[not_at,not_at(top),not_at(bottom)],[pup,pup(p1,bottom)],[not_pup,not_pup(p1,top),not_pup(p1,f1),not_pup(p2,top),not_pup(p2,f1),not_pup(p2,bottom),not_pup(p3,top),not_pup(p3,f1),not_pup(p3,bottom),not_pup(p4,top),not_pup(p4,f1),not_pup(p4,bottom),not_pup(p5,top),not_pup(p5,f1),not_pup(p5,bottom),not_pup(p6,top),not_pup(p6,f1),not_pup(p6,bottom)],[pdown,pdown(p3,f1),pdown(p4,top)],[not_pdown,not_pdown(p1,top),not_pdown(p1,f1),not_pdown(p1,bottom),not_pdown(p2,top),not_pdown(p2,f1),not_pdown(p2,bottom),not_pdown(p3,top),not_pdown(p3,bottom),not_pdown(p4,f1),not_pdown(p4,bottom),not_pdown(p5,top),not_pdown(p5,f1),not_pdown(p5,bottom),not_pdown(p6,top),not_pdown(p6,f1),not_pdown(p6,bottom)],[above,above(top,bottom),above(top,f1),above(f1,bottom)],[not_above,not_above(top,top),not_above(f1,top),not_above(f1,f1),not_above(bottom,top),not_above(bottom,f1),not_above(bottom,bottom)],[pinup],[not_pinup,not_pinup(p1),not_pinup(p2),not_pinup(p3),not_pinup(p4),not_pinup(p5),not_pinup(p6)],[pindown],[not_pindown,not_pindown(p1),not_pindown(p2),not_pindown(p3),not_pindown(p4),not_pindown(p5),not_pindown(p6)],[up],[not_up,not_up],[eq,eq(p1,p1),eq(p2,p2),eq(p3,p3),eq(p4,p4),eq(p5,p5),eq(p6,p6),eq(top,top),eq(f1,f1),eq(bottom,bottom),eq(a,a),eq(a1,a1)],[not_eq,not_eq(p1,p2),not_eq(p1,p3),not_eq(p1,p4),not_eq(p1,p5),not_eq(p1,p6),not_eq(p2,p1),not_eq(p2,p3),not_eq(p2,p4),not_eq(p2,p5),not_eq(p2,p6),not_eq(p3,p1),not_eq(p3,p2),not_eq(p3,p4),not_eq(p3,p5),not_eq(p3,p6),not_eq(p4,p1),not_eq(p4,p2),not_eq(p4,p3),not_eq(p4,p5),not_eq(p4,p6),not_eq(p5,p1),not_eq(p5,p2),not_eq(p5,p3),not_eq(p5,p4),not_eq(p5,p6),not_eq(p6,p1),not_eq(p6,p2),not_eq(p6,p3),not_eq(p6,p4),not_eq(p6,p5),not_eq(top,f1),not_eq(top,bottom),not_eq(f1,top),not_eq(f1,bottom),not_eq(bottom,top),not_eq(bottom,f1),not_eq(a,a1),not_eq(a1,a)]],[[at,at(bottom)],[not_at,not_at(top),not_at(f1)],[pup,pup(p1,bottom),pup(p2,f1)],[not_pup,not_pup(p1,top),not_pup(p1,f1),not_pup(p2,top),not_pup(p2,bottom),not_pup(p3,top),not_pup(p3,f1),not_pup(p3,bottom),not_pup(p4,top),not_pup(p4,f1),not_pup(p4,bottom),not_pup(p5,top),not_pup(p5,f1),not_pup(p5,bottom),not_pup(p6,top),not_pup(p6,f1),not_pup(p6,bottom)],[pdown],[not_pdown,not_pdown(p1,top),not_pdown(p1,f1),not_pdown(p1,bottom),not_pdown(p2,top),not_pdown(p2,f1),not_pdown(p2,bottom),not_pdown(p3,top),not_pdown(p3,f1),not_pdown(p3,bottom),not_pdown(p4,top),not_pdown(p4,f1),not_pdown(p4,bottom),not_pdown(p5,top),not_pdown(p5,f1),not_pdown(p5,bottom),not_pdown(p6,top),not_pdown(p6,f1),not_pdown(p6,bottom)],[above,above(top,bottom),above(top,f1),above(f1,bottom)],[not_above,not_above(top,top),not_above(f1,top),not_above(f1,f1),not_above(bottom,top),not_above(bottom,f1),not_above(bottom,bottom)],[pinup],[not_pinup,not_pinup(p1),not_pinup(p2),not_pinup(p3),not_pinup(p4),not_pinup(p5),not_pinup(p6)],[pindown,pindown(p6)],[not_pindown,not_pindown(p1),not_pindown(p2),not_pindown(p3),not_pindown(p4),not_pindown(p5)],[up],[not_up,not_up],[eq,eq(p1,p1),eq(p2,p2),eq(p3,p3),eq(p4,p4),eq(p5,p5),eq(p6,p6),eq(top,top),eq(f1,f1),eq(bottom,bottom),eq(a,a),eq(a1,a1)],[not_eq,not_eq(p1,p2),not_eq(p1,p3),not_eq(p1,p4),not_eq(p1,p5),not_eq(p1,p6),not_eq(p2,p1),not_eq(p2,p3),not_eq(p2,p4),not_eq(p2,p5),not_eq(p2,p6),not_eq(p3,p1),not_eq(p3,p2),not_eq(p3,p4),not_eq(p3,p5),not_eq(p3,p6),not_eq(p4,p1),not_eq(p4,p2),not_eq(p4,p3),not_eq(p4,p5),not_eq(p4,p6),not_eq(p5,p1),not_eq(p5,p2),not_eq(p5,p3),not_eq(p5,p4),not_eq(p5,p6),not_eq(p6,p1),not_eq(p6,p2),not_eq(p6,p3),not_eq(p6,p4),not_eq(p6,p5),not_eq(top,f1),not_eq(top,bottom),not_eq(f1,top),not_eq(f1,bottom),not_eq(bottom,top),not_eq(bottom,f1),not_eq(a,a1),not_eq(a1,a)]],[[at,at(top)],[not_at,not_at(f1),not_at(bottom)],[pup,pup(p2,f1)],[not_pup,not_pup(p1,top),not_pup(p1,f1),not_pup(p1,bottom),not_pup(p2,top),not_pup(p2,bottom),not_pup(p3,top),not_pup(p3,f1),not_pup(p3,bottom),not_pup(p4,top),not_pup(p4,f1),not_pup(p4,bottom),not_pup(p5,top),not_pup(p5,f1),not_pup(p5,bottom),not_pup(p6,top),not_pup(p6,f1),not_pup(p6,bottom)],[pdown,pdown(p4,top)],[not_pdown,not_pdown(p1,top),not_pdown(p1,f1),not_pdown(p1,bottom),not_pdown(p2,top),not_pdown(p2,f1),not_pdown(p2,bottom),not_pdown(p3,top),not_pdown(p3,f1),not_pdown(p3,bottom),not_pdown(p4,f1),not_pdown(p4,bottom),not_pdown(p5,top),not_pdown(p5,f1),not_pdown(p5,bottom),not_pdown(p6,top),not_pdown(p6,f1),not_pdown(p6,bottom)],[above,above(top,bottom),above(top,f1),above(f1,bottom)],[not_above,not_above(top,top),not_above(f1,top),not_above(f1,f1),not_above(bottom,top),not_above(bottom,f1),not_above(bottom,bottom)],[pinup,pinup(p5)],[not_pinup,not_pinup(p1),not_pinup(p2),not_pinup(p3),not_pinup(p4),not_pinup(p6)],[pindown,pindown(p6)],[not_pindown,not_pindown(p1),not_pindown(p2),not_pindown(p3),not_pindown(p4),not_pindown(p5)],[up],[not_up,not_up],[eq,eq(p1,p1),eq(p2,p2),eq(p3,p3),eq(p4,p4),eq(p5,p5),eq(p6,p6),eq(top,top),eq(f1,f1),eq(bottom,bottom),eq(a,a),eq(a1,a1)],[not_eq,not_eq(p1,p2),not_eq(p1,p3),not_eq(p1,p4),not_eq(p1,p5),not_eq(p1,p6),not_eq(p2,p1),not_eq(p2,p3),not_eq(p2,p4),not_eq(p2,p5),not_eq(p2,p6),not_eq(p3,p1),not_eq(p3,p2),not_eq(p3,p4),not_eq(p3,p5),not_eq(p3,p6),not_eq(p4,p1),not_eq(p4,p2),not_eq(p4,p3),not_eq(p4,p5),not_eq(p4,p6),not_eq(p5,p1),not_eq(p5,p2),not_eq(p5,p3),not_eq(p5,p4),not_eq(p5,p6),not_eq(p6,p1),not_eq(p6,p2),not_eq(p6,p3),not_eq(p6,p4),not_eq(p6,p5),not_eq(top,f1),not_eq(top,bottom),not_eq(f1,top),not_eq(f1,bottom),not_eq(bottom,top),not_eq(bottom,f1),not_eq(a,a1),not_eq(a1,a)]],[[at,at(bottom)],[not_at,not_at(top),not_at(f1)],[pup,pup(p2,f1)],[not_pup,not_pup(p1,top),not_pup(p1,f1),not_pup(p1,bottom),not_pup(p2,top),not_pup(p2,bottom),not_pup(p3,top),not_pup(p3,f1),not_pup(p3,bottom),not_pup(p4,top),not_pup(p4,f1),not_pup(p4,bottom),not_pup(p5,top),not_pup(p5,f1),not_pup(p5,bottom),not_pup(p6,top),not_pup(p6,f1),not_pup(p6,bottom)],[pdown,pdown(p3,f1)],[not_pdown,not_pdown(p1,top),not_pdown(p1,f1),not_pdown(p1,bottom),not_pdown(p2,top),not_pdown(p2,f1),not_pdown(p2,bottom),not_pdown(p3,top),not_pdown(p3,bottom),not_pdown(p4,top),not_pdown(p4,f1),not_pdown(p4,bottom),not_pdown(p5,top),not_pdown(p5,f1),not_pdown(p5,bottom),not_pdown(p6,top),not_pdown(p6,f1),not_pdown(p6,bottom)],[above,above(top,bottom),above(top,f1),above(f1,bottom)],[not_above,not_above(top,top),not_above(f1,top),not_above(f1,f1),not_above(bottom,top),not_above(bottom,f1),not_above(bottom,bottom)],[pinup],[not_pinup,not_pinup(p1),not_pinup(p2),not_pinup(p3),not_pinup(p4),not_pinup(p5),not_pinup(p6)],[pindown,pindown(p6)],[not_pindown,not_pindown(p1),not_pindown(p2),not_pindown(p3),not_pindown(p4),not_pindown(p5)],[up],[not_up,not_up],[eq,eq(p1,p1),eq(p2,p2),eq(p3,p3),eq(p4,p4),eq(p5,p5),eq(p6,p6),eq(top,top),eq(f1,f1),eq(bottom,bottom),eq(a,a),eq(a1,a1)],[not_eq,not_eq(p1,p2),not_eq(p1,p3),not_eq(p1,p4),not_eq(p1,p5),not_eq(p1,p6),not_eq(p2,p1),not_eq(p2,p3),not_eq(p2,p4),not_eq(p2,p5),not_eq(p2,p6),not_eq(p3,p1),not_eq(p3,p2),not_eq(p3,p4),not_eq(p3,p5),not_eq(p3,p6),not_eq(p4,p1),not_eq(p4,p2),not_eq(p4,p3),not_eq(p4,p5),not_eq(p4,p6),not_eq(p5,p1),not_eq(p5,p2),not_eq(p5,p3),not_eq(p5,p4),not_eq(p5,p6),not_eq(p6,p1),not_eq(p6,p2),not_eq(p6,p3),not_eq(p6,p4),not_eq(p6,p5),not_eq(top,f1),not_eq(top,bottom),not_eq(f1,top),not_eq(f1,bottom),not_eq(bottom,top),not_eq(bottom,f1),not_eq(a,a1),not_eq(a1,a)]],[[at,at(bottom)],[not_at,not_at(top),not_at(f1)],[pup,pup(p2,f1)],[not_pup,not_pup(p1,top),not_pup(p1,f1),not_pup(p1,bottom),not_pup(p2,top),not_pup(p2,bottom),not_pup(p3,top),not_pup(p3,f1),not_pup(p3,bottom),not_pup(p4,top),not_pup(p4,f1),not_pup(p4,bottom),not_pup(p5,top),not_pup(p5,f1),not_pup(p5,bottom),not_pup(p6,top),not_pup(p6,f1),not_pup(p6,bottom)],[pdown,pdown(p4,top)],[not_pdown,not_pdown(p1,top),not_pdown(p1,f1),not_pdown(p1,bottom),not_pdown(p2,top),not_pdown(p2,f1),not_pdown(p2,bottom),not_pdown(p3,top),not_pdown(p3,f1),not_pdown(p3,bottom),not_pdown(p4,f1),not_pdown(p4,bottom),not_pdown(p5,top),not_pdown(p5,f1),not_pdown(p5,bottom),not_pdown(p6,top),not_pdown(p6,f1),not_pdown(p6,bottom)],[above,above(top,bottom),above(top,f1),above(f1,bottom)],[not_above,not_above(top,top),not_above(f1,top),not_above(f1,f1),not_above(bottom,top),not_above(bottom,f1),not_above(bottom,bottom)],[pinup],[not_pinup,not_pinup(p1),not_pinup(p2),not_pinup(p3),not_pinup(p4),not_pinup(p5),not_pinup(p6)],[pindown],[not_pindown,not_pindown(p1),not_pindown(p2),not_pindown(p3),not_pindown(p4),not_pindown(p5),not_pindown(p6)],[up],[not_up,not_up],[eq,eq(p1,p1),eq(p2,p2),eq(p3,p3),eq(p4,p4),eq(p5,p5),eq(p6,p6),eq(top,top),eq(f1,f1),eq(bottom,bottom),eq(a,a),eq(a1,a1)],[not_eq,not_eq(p1,p2),not_eq(p1,p3),not_eq(p1,p4),not_eq(p1,p5),not_eq(p1,p6),not_eq(p2,p1),not_eq(p2,p3),not_eq(p2,p4),not_eq(p2,p5),not_eq(p2,p6),not_eq(p3,p1),not_eq(p3,p2),not_eq(p3,p4),not_eq(p3,p5),not_eq(p3,p6),not_eq(p4,p1),not_eq(p4,p2),not_eq(p4,p3),not_eq(p4,p5),not_eq(p4,p6),not_eq(p5,p1),not_eq(p5,p2),not_eq(p5,p3),not_eq(p5,p4),not_eq(p5,p6),not_eq(p6,p1),not_eq(p6,p2),not_eq(p6,p3),not_eq(p6,p4),not_eq(p6,p5),not_eq(top,f1),not_eq(top,bottom),not_eq(f1,top),not_eq(f1,bottom),not_eq(bottom,top),not_eq(bottom,f1),not_eq(a,a1),not_eq(a1,a)]],[[at,at(bottom)],[not_at,not_at(top),not_at(f1)],[pup,pup(p2,f1)],[not_pup,not_pup(p1,top),not_pup(p1,f1),not_pup(p1,bottom),not_pup(p2,top),not_pup(p2,bottom),not_pup(p3,top),not_pup(p3,f1),not_pup(p3,bottom),not_pup(p4,top),not_pup(p4,f1),not_pup(p4,bottom),not_pup(p5,top),not_pup(p5,f1),not_pup(p5,bottom),not_pup(p6,top),not_pup(p6,f1),not_pup(p6,bottom)],[pdown,pdown(p3,f1),pdown(p4,top)],[not_pdown,not_pdown(p1,top),not_pdown(p1,f1),not_pdown(p1,bottom),not_pdown(p2,top),not_pdown(p2,f1),not_pdown(p2,bottom),not_pdown(p3,top),not_pdown(p3,bottom),not_pdown(p4,f1),not_pdown(p4,bottom),not_pdown(p5,top),not_pdown(p5,f1),not_pdown(p5,bottom),not_pdown(p6,top),not_pdown(p6,f1),not_pdown(p6,bottom)],[above,above(top,bottom),above(top,f1),above(f1,bottom)],[not_above,not_above(top,top),not_above(f1,top),not_above(f1,f1),not_above(bottom,top),not_above(bottom,f1),not_above(bottom,bottom)],[pinup,pinup(p5)],[not_pinup,not_pinup(p1),not_pinup(p2),not_pinup(p3),not_pinup(p4),not_pinup(p6)],[pindown],[not_pindown,not_pindown(p1),not_pindown(p2),not_pindown(p3),not_pindown(p4),not_pindown(p5),not_pindown(p6)],[up],[not_up,not_up],[eq,eq(p1,p1),eq(p2,p2),eq(p3,p3),eq(p4,p4),eq(p5,p5),eq(p6,p6),eq(top,top),eq(f1,f1),eq(bottom,bottom),eq(a,a),eq(a1,a1)],[not_eq,not_eq(p1,p2),not_eq(p1,p3),not_eq(p1,p4),not_eq(p1,p5),not_eq(p1,p6),not_eq(p2,p1),not_eq(p2,p3),not_eq(p2,p4),not_eq(p2,p5),not_eq(p2,p6),not_eq(p3,p1),not_eq(p3,p2),not_eq(p3,p4),not_eq(p3,p5),not_eq(p3,p6),not_eq(p4,p1),not_eq(p4,p2),not_eq(p4,p3),not_eq(p4,p5),not_eq(p4,p6),not_eq(p5,p1),not_eq(p5,p2),not_eq(p5,p3),not_eq(p5,p4),not_eq(p5,p6),not_eq(p6,p1),not_eq(p6,p2),not_eq(p6,p3),not_eq(p6,p4),not_eq(p6,p5),not_eq(top,f1),not_eq(top,bottom),not_eq(f1,top),not_eq(f1,bottom),not_eq(bottom,top),not_eq(bottom,f1),not_eq(a,a1),not_eq(a1,a)]],[[at,at(f1)],[not_at,not_at(top),not_at(bottom)],[pup],[not_pup,not_pup(p1,top),not_pup(p1,f1),not_pup(p1,bottom),not_pup(p2,top),not_pup(p2,f1),not_pup(p2,bottom),not_pup(p3,top),not_pup(p3,f1),not_pup(p3,bottom),not_pup(p4,top),not_pup(p4,f1),not_pup(p4,bottom),not_pup(p5,top),not_pup(p5,f1),not_pup(p5,bottom),not_pup(p6,top),not_pup(p6,f1),not_pup(p6,bottom)],[pdown,pdown(p3,f1),pdown(p4,top)],[not_pdown,not_pdown(p1,top),not_pdown(p1,f1),not_pdown(p1,bottom),not_pdown(p2,top),not_pdown(p2,f1),not_pdown(p2,bottom),not_pdown(p3,top),not_pdown(p3,bottom),not_pdown(p4,f1),not_pdown(p4,bottom),not_pdown(p5,top),not_pdown(p5,f1),not_pdown(p5,bottom),not_pdown(p6,top),not_pdown(p6,f1),not_pdown(p6,bottom)],[above,above(top,bottom),above(top,f1),above(f1,bottom)],[not_above,not_above(top,top),not_above(f1,top),not_above(f1,f1),not_above(bottom,top),not_above(bottom,f1),not_above(bottom,bottom)],[pinup,pinup(p5)],[not_pinup,not_pinup(p1),not_pinup(p2),not_pinup(p3),not_pinup(p4),not_pinup(p6)],[pindown],[not_pindown,not_pindown(p1),not_pindown(p2),not_pindown(p3),not_pindown(p4),not_pindown(p5),not_pindown(p6)],[up],[not_up,not_up],[eq,eq(p1,p1),eq(p2,p2),eq(p3,p3),eq(p4,p4),eq(p5,p5),eq(p6,p6),eq(top,top),eq(f1,f1),eq(bottom,bottom),eq(a,a),eq(a1,a1)],[not_eq,not_eq(p1,p2),not_eq(p1,p3),not_eq(p1,p4),not_eq(p1,p5),not_eq(p1,p6),not_eq(p2,p1),not_eq(p2,p3),not_eq(p2,p4),not_eq(p2,p5),not_eq(p2,p6),not_eq(p3,p1),not_eq(p3,p2),not_eq(p3,p4),not_eq(p3,p5),not_eq(p3,p6),not_eq(p4,p1),not_eq(p4,p2),not_eq(p4,p3),not_eq(p4,p5),not_eq(p4,p6),not_eq(p5,p1),not_eq(p5,p2),not_eq(p5,p3),not_eq(p5,p4),not_eq(p5,p6),not_eq(p6,p1),not_eq(p6,p2),not_eq(p6,p3),not_eq(p6,p4),not_eq(p6,p5),not_eq(top,f1),not_eq(top,bottom),not_eq(f1,top),not_eq(f1,bottom),not_eq(bottom,top),not_eq(bottom,f1),not_eq(a,a1),not_eq(a1,a)]],[[at,at(f1)],[not_at,not_at(top),not_at(bottom)],[pup,pup(p2,f1)],[not_pup,not_pup(p1,top),not_pup(p1,f1),not_pup(p1,bottom),not_pup(p2,top),not_pup(p2,bottom),not_pup(p3,top),not_pup(p3,f1),not_pup(p3,bottom),not_pup(p4,top),not_pup(p4,f1),not_pup(p4,bottom),not_pup(p5,top),not_pup(p5,f1),not_pup(p5,bottom),not_pup(p6,top),not_pup(p6,f1),not_pup(p6,bottom)],[pdown,pdown(p3,f1)],[not_pdown,not_pdown(p1,top),not_pdown(p1,f1),not_pdown(p1,bottom),not_pdown(p2,top),not_pdown(p2,f1),not_pdown(p2,bottom),not_pdown(p3,top),not_pdown(p3,bottom),not_pdown(p4,top),not_pdown(p4,f1),not_pdown(p4,bottom),not_pdown(p5,top),not_pdown(p5,f1),not_pdown(p5,bottom),not_pdown(p6,top),not_pdown(p6,f1),not_pdown(p6,bottom)],[above,above(top,bottom),above(top,f1),above(f1,bottom)],[not_above,not_above(top,top),not_above(f1,top),not_above(f1,f1),not_above(bottom,top),not_above(bottom,f1),not_above(bottom,bottom)],[pinup],[not_pinup,not_pinup(p1),not_pinup(p2),not_pinup(p3),not_pinup(p4),not_pinup(p5),not_pinup(p6)],[pindown],[not_pindown,not_pindown(p1),not_pindown(p2),not_pindown(p3),not_pindown(p4),not_pindown(p5),not_pindown(p6)],[up],[not_up,not_up],[eq,eq(p1,p1),eq(p2,p2),eq(p3,p3),eq(p4,p4),eq(p5,p5),eq(p6,p6),eq(top,top),eq(f1,f1),eq(bottom,bottom),eq(a,a),eq(a1,a1)],[not_eq,not_eq(p1,p2),not_eq(p1,p3),not_eq(p1,p4),not_eq(p1,p5),not_eq(p1,p6),not_eq(p2,p1),not_eq(p2,p3),not_eq(p2,p4),not_eq(p2,p5),not_eq(p2,p6),not_eq(p3,p1),not_eq(p3,p2),not_eq(p3,p4),not_eq(p3,p5),not_eq(p3,p6),not_eq(p4,p1),not_eq(p4,p2),not_eq(p4,p3),not_eq(p4,p5),not_eq(p4,p6),not_eq(p5,p1),not_eq(p5,p2),not_eq(p5,p3),not_eq(p5,p4),not_eq(p5,p6),not_eq(p6,p1),not_eq(p6,p2),not_eq(p6,p3),not_eq(p6,p4),not_eq(p6,p5),not_eq(top,f1),not_eq(top,bottom),not_eq(f1,top),not_eq(f1,bottom),not_eq(bottom,top),not_eq(bottom,f1),not_eq(a,a1),not_eq(a1,a)]],[[at,at(bottom)],[not_at,not_at(top),not_at(f1)],[pup,pup(p1,bottom),pup(p2,f1)],[not_pup,not_pup(p1,top),not_pup(p1,f1),not_pup(p2,top),not_pup(p2,bottom),not_pup(p3,top),not_pup(p3,f1),not_pup(p3,bottom),not_pup(p4,top),not_pup(p4,f1),not_pup(p4,bottom),not_pup(p5,top),not_pup(p5,f1),not_pup(p5,bottom),not_pup(p6,top),not_pup(p6,f1),not_pup(p6,bottom)],[pdown,pdown(p3,f1)],[not_pdown,not_pdown(p1,top),not_pdown(p1,f1),not_pdown(p1,bottom),not_pdown(p2,top),not_pdown(p2,f1),not_pdown(p2,bottom),not_pdown(p3,top),not_pdown(p3,bottom),not_pdown(p4,top),not_pdown(p4,f1),not_pdown(p4,bottom),not_pdown(p5,top),not_pdown(p5,f1),not_pdown(p5,bottom),not_pdown(p6,top),not_pdown(p6,f1),not_pdown(p6,bottom)],[above,above(top,bottom),above(top,f1),above(f1,bottom)],[not_above,not_above(top,top),not_above(f1,top),not_above(f1,f1),not_above(bottom,top),not_above(bottom,f1),not_above(bottom,bottom)],[pinup,pinup(p5)],[not_pinup,not_pinup(p1),not_pinup(p2),not_pinup(p3),not_pinup(p4),not_pinup(p6)],[pindown],[not_pindown,not_pindown(p1),not_pindown(p2),not_pindown(p3),not_pindown(p4),not_pindown(p5),not_pindown(p6)],[up],[not_up,not_up],[eq,eq(p1,p1),eq(p2,p2),eq(p3,p3),eq(p4,p4),eq(p5,p5),eq(p6,p6),eq(top,top),eq(f1,f1),eq(bottom,bottom),eq(a,a),eq(a1,a1)],[not_eq,not_eq(p1,p2),not_eq(p1,p3),not_eq(p1,p4),not_eq(p1,p5),not_eq(p1,p6),not_eq(p2,p1),not_eq(p2,p3),not_eq(p2,p4),not_eq(p2,p5),not_eq(p2,p6),not_eq(p3,p1),not_eq(p3,p2),not_eq(p3,p4),not_eq(p3,p5),not_eq(p3,p6),not_eq(p4,p1),not_eq(p4,p2),not_eq(p4,p3),not_eq(p4,p5),not_eq(p4,p6),not_eq(p5,p1),not_eq(p5,p2),not_eq(p5,p3),not_eq(p5,p4),not_eq(p5,p6),not_eq(p6,p1),not_eq(p6,p2),not_eq(p6,p3),not_eq(p6,p4),not_eq(p6,p5),not_eq(top,f1),not_eq(top,bottom),not_eq(f1,top),not_eq(f1,bottom),not_eq(bottom,top),not_eq(bottom,f1),not_eq(a,a1),not_eq(a1,a)]],[[at,at(top)],[not_at,not_at(f1),not_at(bottom)],[pup,pup(p2,f1)],[not_pup,not_pup(p1,top),not_pup(p1,f1),not_pup(p1,bottom),not_pup(p2,top),not_pup(p2,bottom),not_pup(p3,top),not_pup(p3,f1),not_pup(p3,bottom),not_pup(p4,top),not_pup(p4,f1),not_pup(p4,bottom),not_pup(p5,top),not_pup(p5,f1),not_pup(p5,bottom),not_pup(p6,top),not_pup(p6,f1),not_pup(p6,bottom)],[pdown],[not_pdown,not_pdown(p1,top),not_pdown(p1,f1),not_pdown(p1,bottom),not_pdown(p2,top),not_pdown(p2,f1),not_pdown(p2,bottom),not_pdown(p3,top),not_pdown(p3,f1),not_pdown(p3,bottom),not_pdown(p4,top),not_pdown(p4,f1),not_pdown(p4,bottom),not_pdown(p5,top),not_pdown(p5,f1),not_pdown(p5,bottom),not_pdown(p6,top),not_pdown(p6,f1),not_pdown(p6,bottom)],[above,above(top,bottom),above(top,f1),above(f1,bottom)],[not_above,not_above(top,top),not_above(f1,top),not_above(f1,f1),not_above(bottom,top),not_above(bottom,f1),not_above(bottom,bottom)],[pinup],[not_pinup,not_pinup(p1),not_pinup(p2),not_pinup(p3),not_pinup(p4),not_pinup(p5),not_pinup(p6)],[pindown],[not_pindown,not_pindown(p1),not_pindown(p2),not_pindown(p3),not_pindown(p4),not_pindown(p5),not_pindown(p6)],[up],[not_up,not_up],[eq,eq(p1,p1),eq(p2,p2),eq(p3,p3),eq(p4,p4),eq(p5,p5),eq(p6,p6),eq(top,top),eq(f1,f1),eq(bottom,bottom),eq(a,a),eq(a1,a1)],[not_eq,not_eq(p1,p2),not_eq(p1,p3),not_eq(p1,p4),not_eq(p1,p5),not_eq(p1,p6),not_eq(p2,p1),not_eq(p2,p3),not_eq(p2,p4),not_eq(p2,p5),not_eq(p2,p6),not_eq(p3,p1),not_eq(p3,p2),not_eq(p3,p4),not_eq(p3,p5),not_eq(p3,p6),not_eq(p4,p1),not_eq(p4,p2),not_eq(p4,p3),not_eq(p4,p5),not_eq(p4,p6),not_eq(p5,p1),not_eq(p5,p2),not_eq(p5,p3),not_eq(p5,p4),not_eq(p5,p6),not_eq(p6,p1),not_eq(p6,p2),not_eq(p6,p3),not_eq(p6,p4),not_eq(p6,p5),not_eq(top,f1),not_eq(top,bottom),not_eq(f1,top),not_eq(f1,bottom),not_eq(bottom,top),not_eq(bottom,f1),not_eq(a,a1),not_eq(a1,a)]],[[at,at(top)],[not_at,not_at(f1),not_at(bottom)],[pup,pup(p1,bottom)],[not_pup,not_pup(p1,top),not_pup(p1,f1),not_pup(p2,top),not_pup(p2,f1),not_pup(p2,bottom),not_pup(p3,top),not_pup(p3,f1),not_pup(p3,bottom),not_pup(p4,top),not_pup(p4,f1),not_pup(p4,bottom),not_pup(p5,top),not_pup(p5,f1),not_pup(p5,bottom),not_pup(p6,top),not_pup(p6,f1),not_pup(p6,bottom)],[pdown],[not_pdown,not_pdown(p1,top),not_pdown(p1,f1),not_pdown(p1,bottom),not_pdown(p2,top),not_pdown(p2,f1),not_pdown(p2,bottom),not_pdown(p3,top),not_pdown(p3,f1),not_pdown(p3,bottom),not_pdown(p4,top),not_pdown(p4,f1),not_pdown(p4,bottom),not_pdown(p5,top),not_pdown(p5,f1),not_pdown(p5,bottom),not_pdown(p6,top),not_pdown(p6,f1),not_pdown(p6,bottom)],[above,above(top,bottom),above(top,f1),above(f1,bottom)],[not_above,not_above(top,top),not_above(f1,top),not_above(f1,f1),not_above(bottom,top),not_above(bottom,f1),not_above(bottom,bottom)],[pinup],[not_pinup,not_pinup(p1),not_pinup(p2),not_pinup(p3),not_pinup(p4),not_pinup(p5),not_pinup(p6)],[pindown],[not_pindown,not_pindown(p1),not_pindown(p2),not_pindown(p3),not_pindown(p4),not_pindown(p5),not_pindown(p6)],[up],[not_up,not_up],[eq,eq(p1,p1),eq(p2,p2),eq(p3,p3),eq(p4,p4),eq(p5,p5),eq(p6,p6),eq(top,top),eq(f1,f1),eq(bottom,bottom),eq(a,a),eq(a1,a1)],[not_eq,not_eq(p1,p2),not_eq(p1,p3),not_eq(p1,p4),not_eq(p1,p5),not_eq(p1,p6),not_eq(p2,p1),not_eq(p2,p3),not_eq(p2,p4),not_eq(p2,p5),not_eq(p2,p6),not_eq(p3,p1),not_eq(p3,p2),not_eq(p3,p4),not_eq(p3,p5),not_eq(p3,p6),not_eq(p4,p1),not_eq(p4,p2),not_eq(p4,p3),not_eq(p4,p5),not_eq(p4,p6),not_eq(p5,p1),not_eq(p5,p2),not_eq(p5,p3),not_eq(p5,p4),not_eq(p5,p6),not_eq(p6,p1),not_eq(p6,p2),not_eq(p6,p3),not_eq(p6,p4),not_eq(p6,p5),not_eq(top,f1),not_eq(top,bottom),not_eq(f1,top),not_eq(f1,bottom),not_eq(bottom,top),not_eq(bottom,f1),not_eq(a,a1),not_eq(a1,a)]],[[at,at(f1)],[not_at,not_at(top),not_at(bottom)],[pup,pup(p2,f1)],[not_pup,not_pup(p1,top),not_pup(p1,f1),not_pup(p1,bottom),not_pup(p2,top),not_pup(p2,bottom),not_pup(p3,top),not_pup(p3,f1),not_pup(p3,bottom),not_pup(p4,top),not_pup(p4,f1),not_pup(p4,bottom),not_pup(p5,top),not_pup(p5,f1),not_pup(p5,bottom),not_pup(p6,top),not_pup(p6,f1),not_pup(p6,bottom)],[pdown,pdown(p3,f1),pdown(p4,top)],[not_pdown,not_pdown(p1,top),not_pdown(p1,f1),not_pdown(p1,bottom),not_pdown(p2,top),not_pdown(p2,f1),not_pdown(p2,bottom),not_pdown(p3,top),not_pdown(p3,bottom),not_pdown(p4,f1),not_pdown(p4,bottom),not_pdown(p5,top),not_pdown(p5,f1),not_pdown(p5,bottom),not_pdown(p6,top),not_pdown(p6,f1),not_pdown(p6,bottom)],[above,above(top,bottom),above(top,f1),above(f1,bottom)],[not_above,not_above(top,top),not_above(f1,top),not_above(f1,f1),not_above(bottom,top),not_above(bottom,f1),not_above(bottom,bottom)],[pinup],[not_pinup,not_pinup(p1),not_pinup(p2),not_pinup(p3),not_pinup(p4),not_pinup(p5),not_pinup(p6)],[pindown],[not_pindown,not_pindown(p1),not_pindown(p2),not_pindown(p3),not_pindown(p4),not_pindown(p5),not_pindown(p6)],[up],[not_up,not_up],[eq,eq(p1,p1),eq(p2,p2),eq(p3,p3),eq(p4,p4),eq(p5,p5),eq(p6,p6),eq(top,top),eq(f1,f1),eq(bottom,bottom),eq(a,a),eq(a1,a1)],[not_eq,not_eq(p1,p2),not_eq(p1,p3),not_eq(p1,p4),not_eq(p1,p5),not_eq(p1,p6),not_eq(p2,p1),not_eq(p2,p3),not_eq(p2,p4),not_eq(p2,p5),not_eq(p2,p6),not_eq(p3,p1),not_eq(p3,p2),not_eq(p3,p4),not_eq(p3,p5),not_eq(p3,p6),not_eq(p4,p1),not_eq(p4,p2),not_eq(p4,p3),not_eq(p4,p5),not_eq(p4,p6),not_eq(p5,p1),not_eq(p5,p2),not_eq(p5,p3),not_eq(p5,p4),not_eq(p5,p6),not_eq(p6,p1),not_eq(p6,p2),not_eq(p6,p3),not_eq(p6,p4),not_eq(p6,p5),not_eq(top,f1),not_eq(top,bottom),not_eq(f1,top),not_eq(f1,bottom),not_eq(bottom,top),not_eq(bottom,f1),not_eq(a,a1),not_eq(a1,a)]],[[at,at(f1)],[not_at,not_at(top),not_at(bottom)],[pup,pup(p1,bottom)],[not_pup,not_pup(p1,top),not_pup(p1,f1),not_pup(p2,top),not_pup(p2,f1),not_pup(p2,bottom),not_pup(p3,top),not_pup(p3,f1),not_pup(p3,bottom),not_pup(p4,top),not_pup(p4,f1),not_pup(p4,bottom),not_pup(p5,top),not_pup(p5,f1),not_pup(p5,bottom),not_pup(p6,top),not_pup(p6,f1),not_pup(p6,bottom)],[pdown,pdown(p3,f1),pdown(p4,top)],[not_pdown,not_pdown(p1,top),not_pdown(p1,f1),not_pdown(p1,bottom),not_pdown(p2,top),not_pdown(p2,f1),not_pdown(p2,bottom),not_pdown(p3,top),not_pdown(p3,bottom),not_pdown(p4,f1),not_pdown(p4,bottom),not_pdown(p5,top),not_pdown(p5,f1),not_pdown(p5,bottom),not_pdown(p6,top),not_pdown(p6,f1),not_pdown(p6,bottom)],[above,above(top,bottom),above(top,f1),above(f1,bottom)],[not_above,not_above(top,top),not_above(f1,top),not_above(f1,f1),not_above(bottom,top),not_above(bottom,f1),not_above(bottom,bottom)],[pinup],[not_pinup,not_pinup(p1),not_pinup(p2),not_pinup(p3),not_pinup(p4),not_pinup(p5),not_pinup(p6)],[pindown,pindown(p6)],[not_pindown,not_pindown(p1),not_pindown(p2),not_pindown(p3),not_pindown(p4),not_pindown(p5)],[up],[not_up,not_up],[eq,eq(p1,p1),eq(p2,p2),eq(p3,p3),eq(p4,p4),eq(p5,p5),eq(p6,p6),eq(top,top),eq(f1,f1),eq(bottom,bottom),eq(a,a),eq(a1,a1)],[not_eq,not_eq(p1,p2),not_eq(p1,p3),not_eq(p1,p4),not_eq(p1,p5),not_eq(p1,p6),not_eq(p2,p1),not_eq(p2,p3),not_eq(p2,p4),not_eq(p2,p5),not_eq(p2,p6),not_eq(p3,p1),not_eq(p3,p2),not_eq(p3,p4),not_eq(p3,p5),not_eq(p3,p6),not_eq(p4,p1),not_eq(p4,p2),not_eq(p4,p3),not_eq(p4,p5),not_eq(p4,p6),not_eq(p5,p1),not_eq(p5,p2),not_eq(p5,p3),not_eq(p5,p4),not_eq(p5,p6),not_eq(p6,p1),not_eq(p6,p2),not_eq(p6,p3),not_eq(p6,p4),not_eq(p6,p5),not_eq(top,f1),not_eq(top,bottom),not_eq(f1,top),not_eq(f1,bottom),not_eq(bottom,top),not_eq(bottom,f1),not_eq(a,a1),not_eq(a1,a)]],[[at,at(f1)],[not_at,not_at(top),not_at(bottom)],[pup,pup(p1,bottom),pup(p2,f1)],[not_pup,not_pup(p1,top),not_pup(p1,f1),not_pup(p2,top),not_pup(p2,bottom),not_pup(p3,top),not_pup(p3,f1),not_pup(p3,bottom),not_pup(p4,top),not_pup(p4,f1),not_pup(p4,bottom),not_pup(p5,top),not_pup(p5,f1),not_pup(p5,bottom),not_pup(p6,top),not_pup(p6,f1),not_pup(p6,bottom)],[pdown,pdown(p3,f1)],[not_pdown,not_pdown(p1,top),not_pdown(p1,f1),not_pdown(p1,bottom),not_pdown(p2,top),not_pdown(p2,f1),not_pdown(p2,bottom),not_pdown(p3,top),not_pdown(p3,bottom),not_pdown(p4,top),not_pdown(p4,f1),not_pdown(p4,bottom),not_pdown(p5,top),not_pdown(p5,f1),not_pdown(p5,bottom),not_pdown(p6,top),not_pdown(p6,f1),not_pdown(p6,bottom)],[above,above(top,bottom),above(top,f1),above(f1,bottom)],[not_above,not_above(top,top),not_above(f1,top),not_above(f1,f1),not_above(bottom,top),not_above(bottom,f1),not_above(bottom,bottom)],[pinup,pinup(p5)],[not_pinup,not_pinup(p1),not_pinup(p2),not_pinup(p3),not_pinup(p4),not_pinup(p6)],[pindown],[not_pindown,not_pindown(p1),not_pindown(p2),not_pindown(p3),not_pindown(p4),not_pindown(p5),not_pindown(p6)],[up],[not_up,not_up],[eq,eq(p1,p1),eq(p2,p2),eq(p3,p3),eq(p4,p4),eq(p5,p5),eq(p6,p6),eq(top,top),eq(f1,f1),eq(bottom,bottom),eq(a,a),eq(a1,a1)],[not_eq,not_eq(p1,p2),not_eq(p1,p3),not_eq(p1,p4),not_eq(p1,p5),not_eq(p1,p6),not_eq(p2,p1),not_eq(p2,p3),not_eq(p2,p4),not_eq(p2,p5),not_eq(p2,p6),not_eq(p3,p1),not_eq(p3,p2),not_eq(p3,p4),not_eq(p3,p5),not_eq(p3,p6),not_eq(p4,p1),not_eq(p4,p2),not_eq(p4,p3),not_eq(p4,p5),not_eq(p4,p6),not_eq(p5,p1),not_eq(p5,p2),not_eq(p5,p3),not_eq(p5,p4),not_eq(p5,p6),not_eq(p6,p1),not_eq(p6,p2),not_eq(p6,p3),not_eq(p6,p4),not_eq(p6,p5),not_eq(top,f1),not_eq(top,bottom),not_eq(f1,top),not_eq(f1,bottom),not_eq(bottom,top),not_eq(bottom,f1),not_eq(a,a1),not_eq(a1,a)]],[[at,at(top)],[not_at,not_at(f1),not_at(bottom)],[pup,pup(p1,bottom),pup(p2,f1)],[not_pup,not_pup(p1,top),not_pup(p1,f1),not_pup(p2,top),not_pup(p2,bottom),not_pup(p3,top),not_pup(p3,f1),not_pup(p3,bottom),not_pup(p4,top),not_pup(p4,f1),not_pup(p4,bottom),not_pup(p5,top),not_pup(p5,f1),not_pup(p5,bottom),not_pup(p6,top),not_pup(p6,f1),not_pup(p6,bottom)],[pdown,pdown(p4,top)],[not_pdown,not_pdown(p1,top),not_pdown(p1,f1),not_pdown(p1,bottom),not_pdown(p2,top),not_pdown(p2,f1),not_pdown(p2,bottom),not_pdown(p3,top),not_pdown(p3,f1),not_pdown(p3,bottom),not_pdown(p4,f1),not_pdown(p4,bottom),not_pdown(p5,top),not_pdown(p5,f1),not_pdown(p5,bottom),not_pdown(p6,top),not_pdown(p6,f1),not_pdown(p6,bottom)],[above,above(top,bottom),above(top,f1),above(f1,bottom)],[not_above,not_above(top,top),not_above(f1,top),not_above(f1,f1),not_above(bottom,top),not_above(bottom,f1),not_above(bottom,bottom)],[pinup],[not_pinup,not_pinup(p1),not_pinup(p2),not_pinup(p3),not_pinup(p4),not_pinup(p5),not_pinup(p6)],[pindown,pindown(p6)],[not_pindown,not_pindown(p1),not_pindown(p2),not_pindown(p3),not_pindown(p4),not_pindown(p5)],[up],[not_up,not_up],[eq,eq(p1,p1),eq(p2,p2),eq(p3,p3),eq(p4,p4),eq(p5,p5),eq(p6,p6),eq(top,top),eq(f1,f1),eq(bottom,bottom),eq(a,a),eq(a1,a1)],[not_eq,not_eq(p1,p2),not_eq(p1,p3),not_eq(p1,p4),not_eq(p1,p5),not_eq(p1,p6),not_eq(p2,p1),not_eq(p2,p3),not_eq(p2,p4),not_eq(p2,p5),not_eq(p2,p6),not_eq(p3,p1),not_eq(p3,p2),not_eq(p3,p4),not_eq(p3,p5),not_eq(p3,p6),not_eq(p4,p1),not_eq(p4,p2),not_eq(p4,p3),not_eq(p4,p5),not_eq(p4,p6),not_eq(p5,p1),not_eq(p5,p2),not_eq(p5,p3),not_eq(p5,p4),not_eq(p5,p6),not_eq(p6,p1),not_eq(p6,p2),not_eq(p6,p3),not_eq(p6,p4),not_eq(p6,p5),not_eq(top,f1),not_eq(top,bottom),not_eq(f1,top),not_eq(f1,bottom),not_eq(bottom,top),not_eq(bottom,f1),not_eq(a,a1),not_eq(a1,a)]],[[at,at(bottom)],[not_at,not_at(top),not_at(f1)],[pup,pup(p2,f1)],[not_pup,not_pup(p1,top),not_pup(p1,f1),not_pup(p1,bottom),not_pup(p2,top),not_pup(p2,bottom),not_pup(p3,top),not_pup(p3,f1),not_pup(p3,bottom),not_pup(p4,top),not_pup(p4,f1),not_pup(p4,bottom),not_pup(p5,top),not_pup(p5,f1),not_pup(p5,bottom),not_pup(p6,top),not_pup(p6,f1),not_pup(p6,bottom)],[pdown],[not_pdown,not_pdown(p1,top),not_pdown(p1,f1),not_pdown(p1,bottom),not_pdown(p2,top),not_pdown(p2,f1),not_pdown(p2,bottom),not_pdown(p3,top),not_pdown(p3,f1),not_pdown(p3,bottom),not_pdown(p4,top),not_pdown(p4,f1),not_pdown(p4,bottom),not_pdown(p5,top),not_pdown(p5,f1),not_pdown(p5,bottom),not_pdown(p6,top),not_pdown(p6,f1),not_pdown(p6,bottom)],[above,above(top,bottom),above(top,f1),above(f1,bottom)],[not_above,not_above(top,top),not_above(f1,top),not_above(f1,f1),not_above(bottom,top),not_above(bottom,f1),not_above(bottom,bottom)],[pinup],[not_pinup,not_pinup(p1),not_pinup(p2),not_pinup(p3),not_pinup(p4),not_pinup(p5),not_pinup(p6)],[pindown],[not_pindown,not_pindown(p1),not_pindown(p2),not_pindown(p3),not_pindown(p4),not_pindown(p5),not_pindown(p6)],[up],[not_up,not_up],[eq,eq(p1,p1),eq(p2,p2),eq(p3,p3),eq(p4,p4),eq(p5,p5),eq(p6,p6),eq(top,top),eq(f1,f1),eq(bottom,bottom),eq(a,a),eq(a1,a1)],[not_eq,not_eq(p1,p2),not_eq(p1,p3),not_eq(p1,p4),not_eq(p1,p5),not_eq(p1,p6),not_eq(p2,p1),not_eq(p2,p3),not_eq(p2,p4),not_eq(p2,p5),not_eq(p2,p6),not_eq(p3,p1),not_eq(p3,p2),not_eq(p3,p4),not_eq(p3,p5),not_eq(p3,p6),not_eq(p4,p1),not_eq(p4,p2),not_eq(p4,p3),not_eq(p4,p5),not_eq(p4,p6),not_eq(p5,p1),not_eq(p5,p2),not_eq(p5,p3),not_eq(p5,p4),not_eq(p5,p6),not_eq(p6,p1),not_eq(p6,p2),not_eq(p6,p3),not_eq(p6,p4),not_eq(p6,p5),not_eq(top,f1),not_eq(top,bottom),not_eq(f1,top),not_eq(f1,bottom),not_eq(bottom,top),not_eq(bottom,f1),not_eq(a,a1),not_eq(a1,a)]],[[at,at(top)],[not_at,not_at(f1),not_at(bottom)],[pup,pup(p1,bottom)],[not_pup,not_pup(p1,top),not_pup(p1,f1),not_pup(p2,top),not_pup(p2,f1),not_pup(p2,bottom),not_pup(p3,top),not_pup(p3,f1),not_pup(p3,bottom),not_pup(p4,top),not_pup(p4,f1),not_pup(p4,bottom),not_pup(p5,top),not_pup(p5,f1),not_pup(p5,bottom),not_pup(p6,top),not_pup(p6,f1),not_pup(p6,bottom)],[pdown,pdown(p4,top)],[not_pdown,not_pdown(p1,top),not_pdown(p1,f1),not_pdown(p1,bottom),not_pdown(p2,top),not_pdown(p2,f1),not_pdown(p2,bottom),not_pdown(p3,top),not_pdown(p3,f1),not_pdown(p3,bottom),not_pdown(p4,f1),not_pdown(p4,bottom),not_pdown(p5,top),not_pdown(p5,f1),not_pdown(p5,bottom),not_pdown(p6,top),not_pdown(p6,f1),not_pdown(p6,bottom)],[above,above(top,bottom),above(top,f1),above(f1,bottom)],[not_above,not_above(top,top),not_above(f1,top),not_above(f1,f1),not_above(bottom,top),not_above(bottom,f1),not_above(bottom,bottom)],[pinup,pinup(p5)],[not_pinup,not_pinup(p1),not_pinup(p2),not_pinup(p3),not_pinup(p4),not_pinup(p6)],[pindown],[not_pindown,not_pindown(p1),not_pindown(p2),not_pindown(p3),not_pindown(p4),not_pindown(p5),not_pindown(p6)],[up],[not_up,not_up],[eq,eq(p1,p1),eq(p2,p2),eq(p3,p3),eq(p4,p4),eq(p5,p5),eq(p6,p6),eq(top,top),eq(f1,f1),eq(bottom,bottom),eq(a,a),eq(a1,a1)],[not_eq,not_eq(p1,p2),not_eq(p1,p3),not_eq(p1,p4),not_eq(p1,p5),not_eq(p1,p6),not_eq(p2,p1),not_eq(p2,p3),not_eq(p2,p4),not_eq(p2,p5),not_eq(p2,p6),not_eq(p3,p1),not_eq(p3,p2),not_eq(p3,p4),not_eq(p3,p5),not_eq(p3,p6),not_eq(p4,p1),not_eq(p4,p2),not_eq(p4,p3),not_eq(p4,p5),not_eq(p4,p6),not_eq(p5,p1),not_eq(p5,p2),not_eq(p5,p3),not_eq(p5,p4),not_eq(p5,p6),not_eq(p6,p1),not_eq(p6,p2),not_eq(p6,p3),not_eq(p6,p4),not_eq(p6,p5),not_eq(top,f1),not_eq(top,bottom),not_eq(f1,top),not_eq(f1,bottom),not_eq(bottom,top),not_eq(bottom,f1),not_eq(a,a1),not_eq(a1,a)]],[[at,at(top)],[not_at,not_at(f1),not_at(bottom)],[pup,pup(p2,f1)],[not_pup,not_pup(p1,top),not_pup(p1,f1),not_pup(p1,bottom),not_pup(p2,top),not_pup(p2,bottom),not_pup(p3,top),not_pup(p3,f1),not_pup(p3,bottom),not_pup(p4,top),not_pup(p4,f1),not_pup(p4,bottom),not_pup(p5,top),not_pup(p5,f1),not_pup(p5,bottom),not_pup(p6,top),not_pup(p6,f1),not_pup(p6,bottom)],[pdown,pdown(p3,f1),pdown(p4,top)],[not_pdown,not_pdown(p1,top),not_pdown(p1,f1),not_pdown(p1,bottom),not_pdown(p2,top),not_pdown(p2,f1),not_pdown(p2,bottom),not_pdown(p3,top),not_pdown(p3,bottom),not_pdown(p4,f1),not_pdown(p4,bottom),not_pdown(p5,top),not_pdown(p5,f1),not_pdown(p5,bottom),not_pdown(p6,top),not_pdown(p6,f1),not_pdown(p6,bottom)],[above,above(top,bottom),above(top,f1),above(f1,bottom)],[not_above,not_above(top,top),not_above(f1,top),not_above(f1,f1),not_above(bottom,top),not_above(bottom,f1),not_above(bottom,bottom)],[pinup,pinup(p5)],[not_pinup,not_pinup(p1),not_pinup(p2),not_pinup(p3),not_pinup(p4),not_pinup(p6)],[pindown],[not_pindown,not_pindown(p1),not_pindown(p2),not_pindown(p3),not_pindown(p4),not_pindown(p5),not_pindown(p6)],[up],[not_up,not_up],[eq,eq(p1,p1),eq(p2,p2),eq(p3,p3),eq(p4,p4),eq(p5,p5),eq(p6,p6),eq(top,top),eq(f1,f1),eq(bottom,bottom),eq(a,a),eq(a1,a1)],[not_eq,not_eq(p1,p2),not_eq(p1,p3),not_eq(p1,p4),not_eq(p1,p5),not_eq(p1,p6),not_eq(p2,p1),not_eq(p2,p3),not_eq(p2,p4),not_eq(p2,p5),not_eq(p2,p6),not_eq(p3,p1),not_eq(p3,p2),not_eq(p3,p4),not_eq(p3,p5),not_eq(p3,p6),not_eq(p4,p1),not_eq(p4,p2),not_eq(p4,p3),not_eq(p4,p5),not_eq(p4,p6),not_eq(p5,p1),not_eq(p5,p2),not_eq(p5,p3),not_eq(p5,p4),not_eq(p5,p6),not_eq(p6,p1),not_eq(p6,p2),not_eq(p6,p3),not_eq(p6,p4),not_eq(p6,p5),not_eq(top,f1),not_eq(top,bottom),not_eq(f1,top),not_eq(f1,bottom),not_eq(bottom,top),not_eq(bottom,f1),not_eq(a,a1),not_eq(a1,a)]],[[at,at(top)],[not_at,not_at(f1),not_at(bottom)],[pup,pup(p1,bottom)],[not_pup,not_pup(p1,top),not_pup(p1,f1),not_pup(p2,top),not_pup(p2,f1),not_pup(p2,bottom),not_pup(p3,top),not_pup(p3,f1),not_pup(p3,bottom),not_pup(p4,top),not_pup(p4,f1),not_pup(p4,bottom),not_pup(p5,top),not_pup(p5,f1),not_pup(p5,bottom),not_pup(p6,top),not_pup(p6,f1),not_pup(p6,bottom)],[pdown,pdown(p3,f1),pdown(p4,top)],[not_pdown,not_pdown(p1,top),not_pdown(p1,f1),not_pdown(p1,bottom),not_pdown(p2,top),not_pdown(p2,f1),not_pdown(p2,bottom),not_pdown(p3,top),not_pdown(p3,bottom),not_pdown(p4,f1),not_pdown(p4,bottom),not_pdown(p5,top),not_pdown(p5,f1),not_pdown(p5,bottom),not_pdown(p6,top),not_pdown(p6,f1),not_pdown(p6,bottom)],[above,above(top,bottom),above(top,f1),above(f1,bottom)],[not_above,not_above(top,top),not_above(f1,top),not_above(f1,f1),not_above(bottom,top),not_above(bottom,f1),not_above(bottom,bottom)],[pinup,pinup(p5)],[not_pinup,not_pinup(p1),not_pinup(p2),not_pinup(p3),not_pinup(p4),not_pinup(p6)],[pindown,pindown(p6)],[not_pindown,not_pindown(p1),not_pindown(p2),not_pindown(p3),not_pindown(p4),not_pindown(p5)],[up],[not_up,not_up],[eq,eq(p1,p1),eq(p2,p2),eq(p3,p3),eq(p4,p4),eq(p5,p5),eq(p6,p6),eq(top,top),eq(f1,f1),eq(bottom,bottom),eq(a,a),eq(a1,a1)],[not_eq,not_eq(p1,p2),not_eq(p1,p3),not_eq(p1,p4),not_eq(p1,p5),not_eq(p1,p6),not_eq(p2,p1),not_eq(p2,p3),not_eq(p2,p4),not_eq(p2,p5),not_eq(p2,p6),not_eq(p3,p1),not_eq(p3,p2),not_eq(p3,p4),not_eq(p3,p5),not_eq(p3,p6),not_eq(p4,p1),not_eq(p4,p2),not_eq(p4,p3),not_eq(p4,p5),not_eq(p4,p6),not_eq(p5,p1),not_eq(p5,p2),not_eq(p5,p3),not_eq(p5,p4),not_eq(p5,p6),not_eq(p6,p1),not_eq(p6,p2),not_eq(p6,p3),not_eq(p6,p4),not_eq(p6,p5),not_eq(top,f1),not_eq(top,bottom),not_eq(f1,top),not_eq(f1,bottom),not_eq(bottom,top),not_eq(bottom,f1),not_eq(a,a1),not_eq(a1,a)]]]).

